- $x = y \dashv \vdash \map P x \iff \map P y$
for all $P$ in the universe of discourse.
Application to Equality of Sets
Let $S$ be an arbitrary set.
From Set Definition by Predicate, the above formulation can be expressed as:
- $x = y \dashv \vdash x \in S \iff y \in S$
for all $S$ in the universe of discourse.
This is therefore the justification behind the notion of the definition of set equality.
Source of Name
This entry was named for Gottfried Wilhelm von Leibniz.
However, Alfred Tarski notes:
- To regard Leibniz's law here as a definition would make sense only if the meaning of the symbol "$=$" seemed to us less evident than that of expressions [such as 'every property $x$ has, $y$ has'].