Theorem iotasbc5

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

	Ref	Expression
Assertion	iotasbc5	$$⊢\exists !x\phi \to \left(\underset{\dot{}}{[}\left(\iota x|\phi \right)/y\underset{\dot{}}{]}\psi \leftrightarrow \exists y\left(y=\left(\iota x|\phi \right)\wedge \psi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		sbc5	$$⊢\underset{\dot{}}{[}\left(\iota x|\phi \right)/y\underset{\dot{}}{]}\psi \leftrightarrow \exists y\left(y=\left(\iota x|\phi \right)\wedge \psi \right)$$
2	1	a1i	$$⊢\exists !x\phi \to \left(\underset{\dot{}}{[}\left(\iota x|\phi \right)/y\underset{\dot{}}{]}\psi \leftrightarrow \exists y\left(y=\left(\iota x|\phi \right)\wedge \psi \right)\right)$$