This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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