Theorem eu2

Description: An alternate way of defining existential uniqueness. Definition 6.10 of TakeutiZaring p. 26. (Contributed by NM, 8-Jul-1994) (Proof shortened by Wolf Lammen, 2-Dec-2018)

	Ref	Expression
Hypothesis	eu2.nf	|- F/ y ph
Assertion	eu2	|- ( E! x ph <-> ( E. x ph /\ A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )

Proof

Step	Hyp	Ref	Expression
1		eu2.nf	|- F/ y ph
2		df-eu	|- ( E! x ph <-> ( E. x ph /\ E* x ph ) )
3	1	mo3	|- ( E* x ph <-> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )
4	3	anbi2i	|- ( ( E. x ph /\ E* x ph ) <-> ( E. x ph /\ A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
5	2 4	bitri	|- ( E! x ph <-> ( E. x ph /\ A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )