Metamath Proof Explorer

Theorem 2eu3

Description: Double existential uniqueness. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 3-Dec-2001) (Proof shortened by Wolf Lammen, 23-Apr-2023) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 nfmo1 
 |-  F/ y E* y ph
2 1 19.31 
 |-  ( A. y ( E* x ph \/ E* y ph ) <-> ( A. y E* x ph \/ E* y ph ) )
3 2 albii 
 |-  ( A. x A. y ( E* x ph \/ E* y ph ) <-> A. x ( A. y E* x ph \/ E* y ph ) )
4 nfmo1 
 |-  F/ x E* x ph
5 4 nfal 
 |-  F/ x A. y E* x ph
6 5 19.32 
 |-  ( A. x ( A. y E* x ph \/ E* y ph ) <-> ( A. y E* x ph \/ A. x E* y ph ) )
7 3 6 bitri 
 |-  ( A. x A. y ( E* x ph \/ E* y ph ) <-> ( A. y E* x ph \/ A. x E* y ph ) )
8 2eu1 
 |-  ( A. y E* x ph -> ( E! y E! x ph <-> ( E! y E. x ph /\ E! x E. y ph ) ) )
9 8 biimpd 
 |-  ( A. y E* x ph -> ( E! y E! x ph -> ( E! y E. x ph /\ E! x E. y ph ) ) )
10 ancom 
 |-  ( ( E! y E. x ph /\ E! x E. y ph ) <-> ( E! x E. y ph /\ E! y E. x ph ) )
11 9 10 syl6ib 
 |-  ( A. y E* x ph -> ( E! y E! x ph -> ( E! x E. y ph /\ E! y E. x ph ) ) )
12 2eu1 
 |-  ( A. x E* y ph -> ( E! x E! y ph <-> ( E! x E. y ph /\ E! y E. x ph ) ) )
13 12 biimpd 
 |-  ( A. x E* y ph -> ( E! x E! y ph -> ( E! x E. y ph /\ E! y E. x ph ) ) )
14 11 13 jaoa 
 |-  ( ( A. y E* x ph \/ A. x E* y ph ) -> ( ( E! y E! x ph /\ E! x E! y ph ) -> ( E! x E. y ph /\ E! y E. x ph ) ) )
15 14 ancomsd 
 |-  ( ( A. y E* x ph \/ A. x E* y ph ) -> ( ( E! x E! y ph /\ E! y E! x ph ) -> ( E! x E. y ph /\ E! y E. x ph ) ) )
16 2exeu 
 |-  ( ( E! x E. y ph /\ E! y E. x ph ) -> E! x E! y ph )
17 2exeu 
 |-  ( ( E! y E. x ph /\ E! x E. y ph ) -> E! y E! x ph )
18 17 ancoms 
 |-  ( ( E! x E. y ph /\ E! y E. x ph ) -> E! y E! x ph )
19 16 18 jca 
 |-  ( ( E! x E. y ph /\ E! y E. x ph ) -> ( E! x E! y ph /\ E! y E! x ph ) )
20 15 19 impbid1 
 |-  ( ( A. y E* x ph \/ A. x E* y ph ) -> ( ( E! x E! y ph /\ E! y E! x ph ) <-> ( E! x E. y ph /\ E! y E. x ph ) ) )
21 7 20 sylbi 
 |-  ( A. x A. y ( E* x ph \/ E* y ph ) -> ( ( E! x E! y ph /\ E! y E! x ph ) <-> ( E! x E. y ph /\ E! y E. x ph ) ) )