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

Metamath Proof Explorer

Theorem dfeumo

Description: An elementary proof showing the reverse direction of dfmoeu . Here the characterizing expression of existential uniqueness ( eu6 ) is derived from that of uniqueness ( df-mo ). (Contributed by Wolf Lammen, 3-Oct-2023)

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

Proof

Step Hyp Ref Expression
1 ax6ev 
 |-  E. x x = y
2 biimpr 
 |-  ( ( ph <-> x = y ) -> ( x = y -> ph ) )
3 2 aleximi 
 |-  ( A. x ( ph <-> x = y ) -> ( E. x x = y -> E. x ph ) )
4 1 3 mpi 
 |-  ( A. x ( ph <-> x = y ) -> E. x ph )
5 4 exlimiv 
 |-  ( E. y A. x ( ph <-> x = y ) -> E. x ph )
6 5 pm4.71ri 
 |-  ( E. y A. x ( ph <-> x = y ) <-> ( E. x ph /\ E. y A. x ( ph <-> x = y ) ) )
7 abai 
 |-  ( ( E. x ph /\ E. y A. x ( ph <-> x = y ) ) <-> ( E. x ph /\ ( E. x ph -> E. y A. x ( ph <-> x = y ) ) ) )
8 dfmoeu 
 |-  ( ( E. x ph -> E. y A. x ( ph <-> x = y ) ) <-> E. y A. x ( ph -> x = y ) )
9 8 anbi2i 
 |-  ( ( E. x ph /\ ( E. x ph -> E. y A. x ( ph <-> x = y ) ) ) <-> ( E. x ph /\ E. y A. x ( ph -> x = y ) ) )
10 6 7 9 3bitrri 
 |-  ( ( E. x ph /\ E. y A. x ( ph -> x = y ) ) <-> E. y A. x ( ph <-> x = y ) )