Substitutivity of Equality

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $x$ and $y$ be sets.

Let $P \left({x}\right)$ be a well-formed formula of the language of set theory.

Let $P \left({y}\right)$ be the same proposition $P \left({x}\right)$ with some (not necessarily all) free instances of $x$ replaced with free instances of $y$.

Let $=$ denote set equality


$x = y \implies \left({ P \left({x}\right) \iff P \left({y}\right) }\right)$


Proof

By induction on the well-formed parts of $P \left({x}\right)$.

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


Atoms

$x = y \implies \left({ x \in z \iff y \in z }\right)$ by Substitution of Elements
$x = y \implies \left({ z \in x \iff z \in y }\right)$ by definition of Set Equality


Inductive Step for $\implies$

Suppose that $P \left({x}\right)$ is of the form $Q \left({x}\right) \implies R \left({x}\right)$

Furthermore, suppose that:

$x = y \implies \left({ Q \left({x}\right) \iff Q \left({y}\right) }\right)$ and:
$x = y \implies \left({ R \left({x}\right) \iff R \left({y}\right) }\right)$

It follows that:

$x = y \implies \left({ \left({ Q \left({x}\right) \implies R \left({x}\right) }\right) \iff \left({ Q \left({y}\right) \implies R\left({y}\right) }\right) }\right)$
$x = y \implies \left({ P \left({x}\right) \iff P \left({y}\right) }\right)$


Inductive Step for $\neg$

Suppose that $P \left({x}\right)$ is of the form $\neg Q \left({x}\right)$

Furthermore, suppose that:

$x = y \implies \left({ Q \left({x}\right) \iff Q \left({y}\right) }\right)$

It follows that:

$x = y \implies \left({ \neg Q \left({x}\right) \iff \neg Q \left({y}\right) }\right)$
$x = y \implies \left({ P \left({x}\right) \iff P \left({y}\right) }\right)$


Inductive Step for $\forall x:$

Suppose that $P \left({x}\right)$ is of the form $\forall z: Q \left({x, z}\right)$

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\) \(\implies\) \(\displaystyle \left({ Q \left({x, z}\right) \iff Q \left({y, z}\right) }\right)\) Inductive Hypothesis
\(\displaystyle \) \(\implies\) \(\displaystyle \forall z: \left({ Q \left({x, z}\right) \iff Q \left({y, z}\right) }\right)\) Universal Generalization
\(\displaystyle \) \(\implies\) \(\displaystyle \left({ \forall z: Q \left({x, z}\right) \iff \forall z: Q \left({y, z}\right) }\right)\) Predicate Logic manipulation
\(\displaystyle \) \(\implies\) \(\displaystyle \left({ P \left({x}\right) \iff P \left({y}\right) }\right)\) Definition of $P$

$\blacksquare$


Also see


Sources