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

Metamath Proof Explorer

Theorem dfmoeu

Description: An elementary proof of moeu in disguise, connecting an expression characterizing uniqueness ( df-mo ) to that of existential uniqueness ( eu6 ). No particular order of definition is required, as one can be derived from the other. This is shown here and in dfeumo . (Contributed by Wolf Lammen, 27-May-2019)

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

Proof

Step Hyp Ref Expression
1 alnex 
 |-  ( A. x -. ph <-> -. E. x ph )
2 pm2.21 
 |-  ( -. ph -> ( ph -> x = y ) )
3 2 alimi 
 |-  ( A. x -. ph -> A. x ( ph -> x = y ) )
4 1 3 sylbir 
 |-  ( -. E. x ph -> A. x ( ph -> x = y ) )
5 4 19.8ad 
 |-  ( -. E. x ph -> E. y A. x ( ph -> x = y ) )
6 biimp 
 |-  ( ( ph <-> x = y ) -> ( ph -> x = y ) )
7 6 alimi 
 |-  ( A. x ( ph <-> x = y ) -> A. x ( ph -> x = y ) )
8 7 eximi 
 |-  ( E. y A. x ( ph <-> x = y ) -> E. y A. x ( ph -> x = y ) )
9 5 8 ja 
 |-  ( ( E. x ph -> E. y A. x ( ph <-> x = y ) ) -> E. y A. x ( ph -> x = y ) )
10 nfia1 
 |-  F/ x ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) )
11 id 
 |-  ( ph -> ph )
12 ax12v 
 |-  ( x = y -> ( ph -> A. x ( x = y -> ph ) ) )
13 12 com12 
 |-  ( ph -> ( x = y -> A. x ( x = y -> ph ) ) )
14 11 13 embantd 
 |-  ( ph -> ( ( ph -> x = y ) -> A. x ( x = y -> ph ) ) )
15 14 spsd 
 |-  ( ph -> ( A. x ( ph -> x = y ) -> A. x ( x = y -> ph ) ) )
16 15 ancld 
 |-  ( ph -> ( A. x ( ph -> x = y ) -> ( A. x ( ph -> x = y ) /\ A. x ( x = y -> ph ) ) ) )
17 albiim 
 |-  ( A. x ( ph <-> x = y ) <-> ( A. x ( ph -> x = y ) /\ A. x ( x = y -> ph ) ) )
18 16 17 imbitrrdi 
 |-  ( ph -> ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) )
19 10 18 exlimi 
 |-  ( E. x ph -> ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) )
20 19 eximdv 
 |-  ( E. x ph -> ( E. y A. x ( ph -> x = y ) -> E. y A. x ( ph <-> x = y ) ) )
21 20 com12 
 |-  ( E. y A. x ( ph -> x = y ) -> ( E. x ph -> E. y A. x ( ph <-> x = y ) ) )
22 9 21 impbii 
 |-  ( ( E. x ph -> E. y A. x ( ph <-> x = y ) ) <-> E. y A. x ( ph -> x = y ) )