# Substitutivity of Class Equality

## Theorem

Let $A$ and $B$ be classes.

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

Let $\map P B$ be the same proposition $\map P A$ with all instances of $A$ replaced with instances of $B$.

Let $=$ denote class equality.

$A = B \implies \paren {\map P A \iff \map P B}$

## Proof

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

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

### Atoms

First, to prove the statement if $A$ and $B$ are elements of some other class $C$:

 $\ds A = B$ $\leadsto$ $\ds \paren { x = A \iff x = B }$ Class Equality is Transitive $\ds$ $\leadsto$ $\ds \paren {\paren {x = A \land x \in C} \iff \paren {x = B \land x \in C} }$ Propositional Manipulation $\ds$ $\leadsto$ $\ds \forall x: \paren {\paren {x = A \land x \in C} \iff \paren {x = B \land x \in C} }$ Universal Generalisation $\ds$ $\leadsto$ $\ds \paren {A \in C \iff B \in C}$ Characterization of Class Membership

Then, if $A$ and $B$ have $C$ as an element:

 $\ds A = B$ $\leadsto$ $\ds \paren {x \in A \iff x \in B}$ Definition of Class Equality $\ds$ $\leadsto$ $\ds \paren {\paren {x = C \land x \in A} \iff \paren {x = C \land x \in B} }$ Propositional Manipulation $\ds$ $\leadsto$ $\ds \forall x: \paren {\paren {x = C \land x \in A} \iff \paren {x = C \land x \in B} }$ Universal Generalisation $\ds$ $\leadsto$ $\ds \paren {C \in A \iff C \in B}$ Characterization of Class Membership

Recall that for $A \in B$ it has to be the case that $A$ is not a proper class, but a set.

### Inductive Step for $\implies$

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

Furthermore, suppose that:

$A = B \implies \paren {\map Q A \iff \map Q B}$

and:

$A = B \implies \paren {\map R A \iff \map R B}$

It follows that:

$A = B \implies \paren {\paren {\map Q A \implies \map R A} \iff \paren {\map Q B \implies \map R B} }$
$A = B \implies \paren {\map P A \iff \map P B}$

### Inductive Step for $\neg$

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

Furthermore, suppose that:

$A = B \implies \paren {\map Q A \iff \map Q B}$

It follows that:

$A = B \implies \paren {\neg \map Q A \iff \neg \map Q B}$
$A = B \implies \paren {\map P A \iff \map P B}$

### Inductive Step for $\forall x:$

Suppose that $\map P A$ 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 A = B$ $\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 A \iff \map P B}$ Definition of $P$

$\blacksquare$