Substitutivity of Equality

Theorem

Let $x$ and $y$ be sets.

Let $\map P x$ be a well-formed formula of the language of set theory.

Let $\map P y$ be the same proposition $\map P x$ with some (not necessarily all) free instances of $x$ replaced with free instances of $y$.

Let $=$ denote set equality.

$x = y \implies \paren {\map P x \iff \map P y}$

Proof

By induction on the well-formed parts of $\map P x$.

The proof shall use $\implies$ and $\neg$ as the primitive connectives.

Atoms

$x = y \implies \paren {x \in z \iff y \in z}$ by Substitution of Elements.

$x = y \implies \paren {z \in x \iff z \in y}$ by definition of Set Equality.

Inductive Step for $\implies$

Suppose that $\map P x$ is of the form $\map Q x \implies \map R x$

Furthermore, suppose that:

$x = y \implies \paren {\map Q x \iff \map Q y}$

and:

$x = y \implies \paren {\map R x \iff \map R y}$

It follows that:

$x = y \implies \paren {\paren {\map Q x \implies \map R x} \iff \paren {\map Q y \implies \map R y} }$

$x = y \implies \paren {\map P x \iff \map P y}$

Inductive Step for $\neg$

Suppose that $\map P x$ is of the form $\neg \map Q x$

Furthermore, suppose that:

$x = y \implies \paren {\map Q x \iff \map Q y}$

It follows that:

$x = y \implies \paren { \neg \map Q x \iff \neg \map Q y}$

$x = y \implies \paren {\map P x \iff \map P y}$

Inductive Step for $\forall x:$

Suppose that $\map P x$ is of the form $\forall z: \map Q {x, z}$

If $x$ and $z$ are the same variable, then $x$ is a bound variable and the theorem holds trivially.

If $x$ and $z$ are distinct, then:

\(\ds x = y\)

\(\leadsto\)

\(\ds \paren {\map Q {x, z} \iff \map Q {y, z} }\)

Inductive Hypothesis

\(\ds \)

\(\leadsto\)

\(\ds \forall z: \paren {\map Q {x, z} \iff \map Q {y, z} }\)

Universal Generalization

\(\ds \)

\(\leadsto\)

\(\ds \paren {\forall z: \map Q {x, z} \iff \forall z: \map Q {y, z} }\)

Predicate Logic manipulation

\(\ds \)

\(\leadsto\)

\(\ds \paren {\map P x \iff \map P y}\)

Definition of $P$

There is believed to be a mistake here, possibly a typo. In particular: This "Predicate Logic manipulation" is nonsense You can help ProofWiki by reviewing it, and either correcting it or adding some explanatory material as to why you believe it is actually correct after all. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Mistake}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.

$\blacksquare$

Also see

• Axiom:Leibniz's Law

Sources

• 1971: Gaisi Takeuti and Wilson M. Zaring: Introduction to Axiomatic Set Theory: $\S 3.4$