Theorem pm14.12

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

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

Proof

Step	Hyp	Ref	Expression
1		eumo	|- ( E! x ph -> E* x ph )
2		nfv	|- F/ y ph
3	2	mo3	|- ( E* x ph <-> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )
4		sbsbc	|- ( [ y / x ] ph <-> [. y / x ]. ph )
5	4	anbi2i	|- ( ( ph /\ [ y / x ] ph ) <-> ( ph /\ [. y / x ]. ph ) )
6	5	imbi1i	|- ( ( ( ph /\ [ y / x ] ph ) -> x = y ) <-> ( ( ph /\ [. y / x ]. ph ) -> x = y ) )
7	6	2albii	|- ( A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) <-> A. x A. y ( ( ph /\ [. y / x ]. ph ) -> x = y ) )
8	3 7	bitri	|- ( E* x ph <-> A. x A. y ( ( ph /\ [. y / x ]. ph ) -> x = y ) )
9	1 8	sylib	|- ( E! x ph -> A. x A. y ( ( ph /\ [. y / x ]. ph ) -> x = y ) )