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

 $\displaystyle x = y$ $\leadsto$ $\displaystyle \paren {\map Q {x, z} \iff \map Q {y, z} }$ Inductive Hypothesis $\displaystyle$ $\leadsto$ $\displaystyle \forall z: \paren {\map Q {x, z} \iff \map Q {y, z} }$ Universal Generalization $\displaystyle$ $\leadsto$ $\displaystyle \paren {\forall z: \map Q {x, z} \iff \forall z: \map Q {y, z} }$ Predicate Logic manipulation $\displaystyle$ $\leadsto$ $\displaystyle \paren {\map P x \iff \map P y}$ Definition of $P$

$\blacksquare$