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

## Also see

## Sources

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