Substitutivity of Equality

From ProofWiki
Jump to navigation Jump to search

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$


Also see


Sources