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

Metamath Proof Explorer

Theorem eu6lem

Description: Lemma of eu6im . A dissection of an idiom characterizing existential uniqueness. (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) Extract common proof lines. (Revised by Wolf Lammen, 3-Mar-2023)

Ref Expression
Assertion eu6lem 
|- ( E. y A. x ( ph <-> x = y ) <-> ( E. y A. x ( x = y -> ph ) /\ E. z A. x ( ph -> x = z ) ) )

Proof

Step Hyp Ref Expression
1 19.42v 
 |-  ( E. z ( A. x ( ph <-> x = y ) /\ y = z ) <-> ( A. x ( ph <-> x = y ) /\ E. z y = z ) )
2 alsyl 
 |-  ( ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = z ) ) -> A. x ( x = y -> x = z ) )
3 equvelv 
 |-  ( A. x ( x = y -> x = z ) <-> y = z )
4 2 3 sylib 
 |-  ( ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = z ) ) -> y = z )
5 4 pm4.71i 
 |-  ( ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = z ) ) <-> ( ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = z ) ) /\ y = z ) )
6 albiim 
 |-  ( A. x ( ph <-> x = y ) <-> ( A. x ( ph -> x = y ) /\ A. x ( x = y -> ph ) ) )
7 6 biancomi 
 |-  ( A. x ( ph <-> x = y ) <-> ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = y ) ) )
8 equequ2 
 |-  ( y = z -> ( x = y <-> x = z ) )
9 8 imbi2d 
 |-  ( y = z -> ( ( ph -> x = y ) <-> ( ph -> x = z ) ) )
10 9 albidv 
 |-  ( y = z -> ( A. x ( ph -> x = y ) <-> A. x ( ph -> x = z ) ) )
11 10 anbi2d 
 |-  ( y = z -> ( ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = y ) ) <-> ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = z ) ) ) )
12 7 11 bitrid 
 |-  ( y = z -> ( A. x ( ph <-> x = y ) <-> ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = z ) ) ) )
13 12 pm5.32ri 
 |-  ( ( A. x ( ph <-> x = y ) /\ y = z ) <-> ( ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = z ) ) /\ y = z ) )
14 5 13 bitr4i 
 |-  ( ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = z ) ) <-> ( A. x ( ph <-> x = y ) /\ y = z ) )
15 14 exbii 
 |-  ( E. z ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = z ) ) <-> E. z ( A. x ( ph <-> x = y ) /\ y = z ) )
16 ax6evr 
 |-  E. z y = z
17 16 biantru 
 |-  ( A. x ( ph <-> x = y ) <-> ( A. x ( ph <-> x = y ) /\ E. z y = z ) )
18 1 15 17 3bitr4ri 
 |-  ( A. x ( ph <-> x = y ) <-> E. z ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = z ) ) )
19 18 exbii 
 |-  ( E. y A. x ( ph <-> x = y ) <-> E. y E. z ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = z ) ) )
20 exdistrv 
 |-  ( E. y E. z ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = z ) ) <-> ( E. y A. x ( x = y -> ph ) /\ E. z A. x ( ph -> x = z ) ) )
21 19 20 bitri 
 |-  ( E. y A. x ( ph <-> x = y ) <-> ( E. y A. x ( x = y -> ph ) /\ E. z A. x ( ph -> x = z ) ) )