Theorem eu6

Description: Alternate definition of the unique existential quantifier df-eu not using the at-most-one quantifier. (Contributed by NM, 12-Aug-1993) This used to be the definition of the unique existential quantifier, while df-eu was then proved as dfeu . (Revised by BJ, 30-Sep-2022) (Proof shortened by Wolf Lammen, 3-Jan-2023) Remove use of ax-11 . (Revised by SN, 21-Sep-2023)

	Ref	Expression
Assertion	eu6	|- ( E! x ph <-> E. y A. x ( ph <-> x = y ) )

Proof

Step	Hyp	Ref	Expression
1		dfmoeu	|- ( ( E. x ph -> E. y A. x ( ph <-> x = y ) ) <-> E. y A. x ( ph -> x = y ) )
2	1	anbi2i	|- ( ( E. x ph /\ ( E. x ph -> E. y A. x ( ph <-> x = y ) ) ) <-> ( E. x ph /\ E. y A. x ( ph -> x = y ) ) )
3		abai	|- ( ( E. x ph /\ E. y A. x ( ph <-> x = y ) ) <-> ( E. x ph /\ ( E. x ph -> E. y A. x ( ph <-> x = y ) ) ) )
4		eu3v	|- ( E! x ph <-> ( E. x ph /\ E. y A. x ( ph -> x = y ) ) )
5	2 3 4	3bitr4ri	|- ( E! x ph <-> ( E. x ph /\ E. y A. x ( ph <-> x = y ) ) )
6		abai	|- ( ( E. y A. x ( ph <-> x = y ) /\ E. x ph ) <-> ( E. y A. x ( ph <-> x = y ) /\ ( E. y A. x ( ph <-> x = y ) -> E. x ph ) ) )
7		ancom	|- ( ( E. x ph /\ E. y A. x ( ph <-> x = y ) ) <-> ( E. y A. x ( ph <-> x = y ) /\ E. x ph ) )
8		biimpr	|- ( ( ph <-> x = y ) -> ( x = y -> ph ) )
9	8	alimi	|- ( A. x ( ph <-> x = y ) -> A. x ( x = y -> ph ) )
10	9	eximi	|- ( E. y A. x ( ph <-> x = y ) -> E. y A. x ( x = y -> ph ) )
11		exsbim	|- ( E. y A. x ( x = y -> ph ) -> E. x ph )
12	10 11	syl	|- ( E. y A. x ( ph <-> x = y ) -> E. x ph )
13	12	biantru	|- ( E. y A. x ( ph <-> x = y ) <-> ( E. y A. x ( ph <-> x = y ) /\ ( E. y A. x ( ph <-> x = y ) -> E. x ph ) ) )
14	6 7 13	3bitr4i	|- ( ( E. x ph /\ E. y A. x ( ph <-> x = y ) ) <-> E. y A. x ( ph <-> x = y ) )
15	5 14	bitri	|- ( E! x ph <-> E. y A. x ( ph <-> x = y ) )