# 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$ |

$\blacksquare$

## Also see

## Sources

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