Theorem pm14.24

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

	Ref	Expression
Assertion	pm14.24	|- ( E! x ph -> A. y ( [. y / x ]. ph <-> y = ( iota x ph ) ) )

Proof

Step	Hyp	Ref	Expression
1		nfeu1	|- F/ x E! x ph
2		nfsbc1v	|- F/ x [. y / x ]. ph
3		pm14.12	|- ( E! x ph -> A. x A. y ( ( ph /\ [. y / x ]. ph ) -> x = y ) )
4	3	19.21bbi	|- ( E! x ph -> ( ( ph /\ [. y / x ]. ph ) -> x = y ) )
5	4	ancomsd	|- ( E! x ph -> ( ( [. y / x ]. ph /\ ph ) -> x = y ) )
6	5	expdimp	|- ( ( E! x ph /\ [. y / x ]. ph ) -> ( ph -> x = y ) )
7		pm13.13b	|- ( ( [. y / x ]. ph /\ x = y ) -> ph )
8	7	ex	|- ( [. y / x ]. ph -> ( x = y -> ph ) )
9	8	adantl	|- ( ( E! x ph /\ [. y / x ]. ph ) -> ( x = y -> ph ) )
10	6 9	impbid	|- ( ( E! x ph /\ [. y / x ]. ph ) -> ( ph <-> x = y ) )
11	10	ex	|- ( E! x ph -> ( [. y / x ]. ph -> ( ph <-> x = y ) ) )
12	1 2 11	alrimd	|- ( E! x ph -> ( [. y / x ]. ph -> A. x ( ph <-> x = y ) ) )
13		iotaval	|- ( A. x ( ph <-> x = y ) -> ( iota x ph ) = y )
14	13	eqcomd	|- ( A. x ( ph <-> x = y ) -> y = ( iota x ph ) )
15	12 14	syl6	|- ( E! x ph -> ( [. y / x ]. ph -> y = ( iota x ph ) ) )
16		iota4	|- ( E! x ph -> [. ( iota x ph ) / x ]. ph )
17		dfsbcq	|- ( y = ( iota x ph ) -> ( [. y / x ]. ph <-> [. ( iota x ph ) / x ]. ph ) )
18	16 17	syl5ibrcom	|- ( E! x ph -> ( y = ( iota x ph ) -> [. y / x ]. ph ) )
19	15 18	impbid	|- ( E! x ph -> ( [. y / x ]. ph <-> y = ( iota x ph ) ) )
20	19	alrimiv	|- ( E! x ph -> A. y ( [. y / x ]. ph <-> y = ( iota x ph ) ) )