Metamath Proof Explorer


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 ) )