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$