Theorem pm14.24

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

	Ref	Expression
Assertion	pm14.24	$$⊢\exists !x\phi \to \forall y\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow y=\left(\iota x|\phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfeu1	$$⊢Ⅎx\exists !x\phi$$
2		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi$$
3		pm14.12	$$⊢\exists !x\phi \to \forall x\forall y\left(\left(\phi \wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\to x=y\right)$$
4	3	19.21bbi	$$⊢\exists !x\phi \to \left(\left(\phi \wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\to x=y\right)$$
5	4	ancomsd	$$⊢\exists !x\phi \to \left(\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \wedge \phi \right)\to x=y\right)$$
6	5	expdimp	$$⊢\left(\exists !x\phi \wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\to \left(\phi \to x=y\right)$$
7		pm13.13b	$$⊢\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \wedge x=y\right)\to \phi$$
8	7	ex	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \to \left(x=y\to \phi \right)$$
9	8	adantl	$$⊢\left(\exists !x\phi \wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\to \left(x=y\to \phi \right)$$
10	6 9	impbid	$$⊢\left(\exists !x\phi \wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\to \left(\phi \leftrightarrow x=y\right)$$
11	10	ex	$$⊢\exists !x\phi \to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \to \left(\phi \leftrightarrow x=y\right)\right)$$
12	1 2 11	alrimd	$$⊢\exists !x\phi \to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \to \forall x\left(\phi \leftrightarrow x=y\right)\right)$$
13		iotaval	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \left(\iota x|\phi \right)=y$$
14	13	eqcomd	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to y=\left(\iota x|\phi \right)$$
15	12 14	syl6	$$⊢\exists !x\phi \to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \to y=\left(\iota x|\phi \right)\right)$$
16		iota4	$$⊢\exists !x\phi \to \underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\phi$$
17		dfsbcq	$$⊢y=\left(\iota x|\phi \right)\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\phi \right)$$
18	16 17	syl5ibrcom	$$⊢\exists !x\phi \to \left(y=\left(\iota x|\phi \right)\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)$$
19	15 18	impbid	$$⊢\exists !x\phi \to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow y=\left(\iota x|\phi \right)\right)$$
20	19	alrimiv	$$⊢\exists !x\phi \to \forall y\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow y=\left(\iota x|\phi \right)\right)$$