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

Metamath Proof Explorer

Theorem 2eu1

Description: Double existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker 2eu1v when possible. (Contributed by NM, 3-Dec-2001) (Proof shortened by Wolf Lammen, 23-Apr-2023) (New usage is discouraged.)

Ref Expression
Assertion 2eu1 
|- ( A. x E* y ph -> ( E! x E! y ph <-> ( E! x E. y ph /\ E! y E. x ph ) ) )

Proof

Step Hyp Ref Expression
1 2eu2ex 
 |-  ( E! x E! y ph -> E. x E. y ph )
2 moeu 
 |-  ( E* y ph <-> ( E. y ph -> E! y ph ) )
3 2 albii 
 |-  ( A. x E* y ph <-> A. x ( E. y ph -> E! y ph ) )
4 euim 
 |-  ( ( E. x E. y ph /\ A. x ( E. y ph -> E! y ph ) ) -> ( E! x E! y ph -> E! x E. y ph ) )
5 3 4 sylan2b 
 |-  ( ( E. x E. y ph /\ A. x E* y ph ) -> ( E! x E! y ph -> E! x E. y ph ) )
6 5 ex 
 |-  ( E. x E. y ph -> ( A. x E* y ph -> ( E! x E! y ph -> E! x E. y ph ) ) )
7 1 6 syl 
 |-  ( E! x E! y ph -> ( A. x E* y ph -> ( E! x E! y ph -> E! x E. y ph ) ) )
8 7 pm2.43b 
 |-  ( A. x E* y ph -> ( E! x E! y ph -> E! x E. y ph ) )
9 2euswap 
 |-  ( A. x E* y ph -> ( E! x E. y ph -> E! y E. x ph ) )
10 8 9 syld 
 |-  ( A. x E* y ph -> ( E! x E! y ph -> E! y E. x ph ) )
11 8 10 jcad 
 |-  ( A. x E* y ph -> ( E! x E! y ph -> ( E! x E. y ph /\ E! y E. x ph ) ) )
12 2exeu 
 |-  ( ( E! x E. y ph /\ E! y E. x ph ) -> E! x E! y ph )
13 11 12 impbid1 
 |-  ( A. x E* y ph -> ( E! x E! y ph <-> ( E! x E. y ph /\ E! y E. x ph ) ) )