Theorem sbaniota

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

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

Proof

Step	Hyp	Ref	Expression
1		eupickbi	$$⊢\exists !x\phi \to \left(\exists x\left(\phi \wedge \psi \right)\leftrightarrow \forall x\left(\phi \to \psi \right)\right)$$
2		sbiota1	$$⊢\exists !x\phi \to \left(\forall x\left(\phi \to \psi \right)\leftrightarrow \underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\psi \right)$$
3	1 2	bitrd	$$⊢\exists !x\phi \to \left(\exists x\left(\phi \wedge \psi \right)\leftrightarrow \underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\psi \right)$$