Substitution Property of Equality

Theorem

Let $\map F z$ be an expression of the variable $z$.

Then:

$\forall x, y: x = y \implies \map F x = \map F y$.

Proof

By the tableau method of natural deduction:

$\forall x, y: x = y \implies \map F x = \map F y$

Line		Pool	Formula	Rule	Depends upon	Notes
1		1	$x = y$	Assumption
2		1	$\map F x = \map F x \iff \map F x = \map F y$	Leibniz's Law	1	$\map P a := \map F x = \map F a$
3		1	$\map F x = \map F x \implies \map F x = \map F y$	Biconditional Elimination	2
4			$\forall a: a = a$	Theorem Introduction	(None)	Equality is Reflexive
5			$\map F x = \map F y$	Universal Instantiation	4
6		1	$\map F x = \map F y$	Modus Ponendo Ponens	3, 5
7			$x = y \implies \map F x = \map F y$	Rule of Implication	1-6
8			$\forall x, y: x = y \implies \map F x = \map F y$	Universal Generalization	7