Theorem iotasbc

Description: Definition *14.01 in WhiteheadRussell p. 184. In Principia Mathematica, Russell and Whitehead define iota in terms of a function of ( iota x ph ) . Their definition differs in that a function of ( iota x ph ) evaluates to "false" when there isn't a single x that satisfies ph . (Contributed by Andrew Salmon, 11-Jul-2011)

	Ref	Expression
Assertion	iotasbc	$$⊢\exists !x\phi \to \left(\underset{\dot{}}{[}\left(\iota x|\phi \right)/y\underset{\dot{}}{]}\psi \leftrightarrow \exists y\left(\forall x\left(\phi \leftrightarrow x=y\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		iotaexeu	$$⊢\exists !x\phi \to \left(\iota x|\phi \right)\in \mathrm{V}$$
3		eueq	$$⊢\left(\iota x|\phi \right)\in \mathrm{V}\leftrightarrow \exists !yy=\left(\iota x|\phi \right)$$
4	2 3	sylib	$$⊢\exists !x\phi \to \exists !yy=\left(\iota x|\phi \right)$$
5		eu6	$$⊢\exists !x\phi \leftrightarrow \exists y\forall x\left(\phi \leftrightarrow x=y\right)$$
6		iotaval	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \left(\iota x|\phi \right)=y$$
7	6	eqcomd	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to y=\left(\iota x|\phi \right)$$
8	7	ancri	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \left(y=\left(\iota x|\phi \right)\wedge \forall x\left(\phi \leftrightarrow x=y\right)\right)$$
9	8	eximi	$$⊢\exists y\forall x\left(\phi \leftrightarrow x=y\right)\to \exists y\left(y=\left(\iota x|\phi \right)\wedge \forall x\left(\phi \leftrightarrow x=y\right)\right)$$
10	5 9	sylbi	$$⊢\exists !x\phi \to \exists y\left(y=\left(\iota x|\phi \right)\wedge \forall x\left(\phi \leftrightarrow x=y\right)\right)$$
11		eupick	$$⊢\left(\exists !yy=\left(\iota x|\phi \right)\wedge \exists y\left(y=\left(\iota x|\phi \right)\wedge \forall x\left(\phi \leftrightarrow x=y\right)\right)\right)\to \left(y=\left(\iota x|\phi \right)\to \forall x\left(\phi \leftrightarrow x=y\right)\right)$$
12	4 10 11	syl2anc	$$⊢\exists !x\phi \to \left(y=\left(\iota x|\phi \right)\to \forall x\left(\phi \leftrightarrow x=y\right)\right)$$
13	12 7	impbid1	$$⊢\exists !x\phi \to \left(y=\left(\iota x|\phi \right)\leftrightarrow \forall x\left(\phi \leftrightarrow x=y\right)\right)$$
14	13	anbi1d	$$⊢\exists !x\phi \to \left(\left(y=\left(\iota x|\phi \right)\wedge \psi \right)\leftrightarrow \left(\forall x\left(\phi \leftrightarrow x=y\right)\wedge \psi \right)\right)$$
15	14	exbidv	$$⊢\exists !x\phi \to \left(\exists y\left(y=\left(\iota x|\phi \right)\wedge \psi \right)\leftrightarrow \exists y\left(\forall x\left(\phi \leftrightarrow x=y\right)\wedge \psi \right)\right)$$
16	1 15	bitrid	$$⊢\exists !x\phi \to \left(\underset{\dot{}}{[}\left(\iota x|\phi \right)/y\underset{\dot{}}{]}\psi \leftrightarrow \exists y\left(\forall x\left(\phi \leftrightarrow x=y\right)\wedge \psi \right)\right)$$