Theorem iotavalsb

Description: Theorem *14.242 in WhiteheadRussell p. 192. (Contributed by Andrew Salmon, 11-Jul-2011)

	Ref	Expression
Assertion	iotavalsb	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \left(\underset{\dot{}}{[}y/z\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}\left(\iota x|\phi \right)/z\underset{\dot{}}{]}\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		19.8a	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \exists y\forall x\left(\phi \leftrightarrow x=y\right)$$
2		eu6	$$⊢\exists !x\phi \leftrightarrow \exists y\forall x\left(\phi \leftrightarrow x=y\right)$$
3		iotavalb	$$⊢\exists !x\phi \to \left(\forall x\left(\phi \leftrightarrow x=y\right)\leftrightarrow \left(\iota x|\phi \right)=y\right)$$
4		dfsbcq	$$⊢y=\left(\iota x|\phi \right)\to \left(\underset{\dot{}}{[}y/z\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}\left(\iota x|\phi \right)/z\underset{\dot{}}{]}\psi \right)$$
5	4	eqcoms	$$⊢\left(\iota x|\phi \right)=y\to \left(\underset{\dot{}}{[}y/z\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}\left(\iota x|\phi \right)/z\underset{\dot{}}{]}\psi \right)$$
6	3 5	syl6bi	$$⊢\exists !x\phi \to \left(\forall x\left(\phi \leftrightarrow x=y\right)\to \left(\underset{\dot{}}{[}y/z\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}\left(\iota x|\phi \right)/z\underset{\dot{}}{]}\psi \right)\right)$$
7	2 6	sylbir	$$⊢\exists y\forall x\left(\phi \leftrightarrow x=y\right)\to \left(\forall x\left(\phi \leftrightarrow x=y\right)\to \left(\underset{\dot{}}{[}y/z\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}\left(\iota x|\phi \right)/z\underset{\dot{}}{]}\psi \right)\right)$$
8	1 7	mpcom	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \left(\underset{\dot{}}{[}y/z\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}\left(\iota x|\phi \right)/z\underset{\dot{}}{]}\psi \right)$$