Metamath Proof Explorer

Theorem 2eu6

Description: Two equivalent expressions for double existential uniqueness. (Contributed by NM, 2-Feb-2005) (Revised by Mario Carneiro, 17-Oct-2016) (Proof shortened by Wolf Lammen, 2-Oct-2019)

Ref Expression
Assertion 2eu6 
|- ( ( E! x E. y ph /\ E! y E. x ph ) <-> E. z E. w A. x A. y ( ph <-> ( x = z /\ y = w ) ) )

Proof

Step Hyp Ref Expression
1 2eu4 
 |-  ( ( E! x E. y ph /\ E! y E. x ph ) <-> ( E. x E. y ph /\ E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )
2 nfia1 
 |-  F/ x ( A. x A. y ( ph -> ( x = z /\ y = w ) ) -> A. x A. y ( ph <-> ( x = z /\ y = w ) ) )
3 nfa1 
 |-  F/ y A. y ( ph -> ( x = z /\ y = w ) )
4 nfv 
 |-  F/ y x = z
5 simpl 
 |-  ( ( x = z /\ y = w ) -> x = z )
6 5 imim2i 
 |-  ( ( ph -> ( x = z /\ y = w ) ) -> ( ph -> x = z ) )
7 6 sps 
 |-  ( A. y ( ph -> ( x = z /\ y = w ) ) -> ( ph -> x = z ) )
8 3 4 7 exlimd 
 |-  ( A. y ( ph -> ( x = z /\ y = w ) ) -> ( E. y ph -> x = z ) )
9 ax12v 
 |-  ( x = z -> ( E. y ph -> A. x ( x = z -> E. y ph ) ) )
10 8 9 syli 
 |-  ( A. y ( ph -> ( x = z /\ y = w ) ) -> ( E. y ph -> A. x ( x = z -> E. y ph ) ) )
11 10 com12 
 |-  ( E. y ph -> ( A. y ( ph -> ( x = z /\ y = w ) ) -> A. x ( x = z -> E. y ph ) ) )
12 11 spsd 
 |-  ( E. y ph -> ( A. x A. y ( ph -> ( x = z /\ y = w ) ) -> A. x ( x = z -> E. y ph ) ) )
13 nfs1v 
 |-  F/ y [ w / y ] ph
14 simpr 
 |-  ( ( x = z /\ y = w ) -> y = w )
15 14 imim2i 
 |-  ( ( ph -> ( x = z /\ y = w ) ) -> ( ph -> y = w ) )
16 sbequ1 
 |-  ( y = w -> ( ph -> [ w / y ] ph ) )
17 15 16 syli 
 |-  ( ( ph -> ( x = z /\ y = w ) ) -> ( ph -> [ w / y ] ph ) )
18 17 sps 
 |-  ( A. y ( ph -> ( x = z /\ y = w ) ) -> ( ph -> [ w / y ] ph ) )
19 3 13 18 exlimd 
 |-  ( A. y ( ph -> ( x = z /\ y = w ) ) -> ( E. y ph -> [ w / y ] ph ) )
20 19 imim2d 
 |-  ( A. y ( ph -> ( x = z /\ y = w ) ) -> ( ( x = z -> E. y ph ) -> ( x = z -> [ w / y ] ph ) ) )
21 20 al2imi 
 |-  ( A. x A. y ( ph -> ( x = z /\ y = w ) ) -> ( A. x ( x = z -> E. y ph ) -> A. x ( x = z -> [ w / y ] ph ) ) )
22 sb6 
 |-  ( [ z / x ] [ w / y ] ph <-> A. x ( x = z -> [ w / y ] ph ) )
23 2sb6 
 |-  ( [ z / x ] [ w / y ] ph <-> A. x A. y ( ( x = z /\ y = w ) -> ph ) )
24 22 23 bitr3i 
 |-  ( A. x ( x = z -> [ w / y ] ph ) <-> A. x A. y ( ( x = z /\ y = w ) -> ph ) )
25 21 24 imbitrdi 
 |-  ( A. x A. y ( ph -> ( x = z /\ y = w ) ) -> ( A. x ( x = z -> E. y ph ) -> A. x A. y ( ( x = z /\ y = w ) -> ph ) ) )
26 12 25 sylcom 
 |-  ( E. y ph -> ( A. x A. y ( ph -> ( x = z /\ y = w ) ) -> A. x A. y ( ( x = z /\ y = w ) -> ph ) ) )
27 26 ancld 
 |-  ( E. y ph -> ( A. x A. y ( ph -> ( x = z /\ y = w ) ) -> ( A. x A. y ( ph -> ( x = z /\ y = w ) ) /\ A. x A. y ( ( x = z /\ y = w ) -> ph ) ) ) )
28 2albiim 
 |-  ( A. x A. y ( ph <-> ( x = z /\ y = w ) ) <-> ( A. x A. y ( ph -> ( x = z /\ y = w ) ) /\ A. x A. y ( ( x = z /\ y = w ) -> ph ) ) )
29 27 28 imbitrrdi 
 |-  ( E. y ph -> ( A. x A. y ( ph -> ( x = z /\ y = w ) ) -> A. x A. y ( ph <-> ( x = z /\ y = w ) ) ) )
30 2 29 exlimi 
 |-  ( E. x E. y ph -> ( A. x A. y ( ph -> ( x = z /\ y = w ) ) -> A. x A. y ( ph <-> ( x = z /\ y = w ) ) ) )
31 30 2eximdv 
 |-  ( E. x E. y ph -> ( E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) -> E. z E. w A. x A. y ( ph <-> ( x = z /\ y = w ) ) ) )
32 31 imp 
 |-  ( ( E. x E. y ph /\ E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) -> E. z E. w A. x A. y ( ph <-> ( x = z /\ y = w ) ) )
33 biimpr 
 |-  ( ( ph <-> ( x = z /\ y = w ) ) -> ( ( x = z /\ y = w ) -> ph ) )
34 33 2alimi 
 |-  ( A. x A. y ( ph <-> ( x = z /\ y = w ) ) -> A. x A. y ( ( x = z /\ y = w ) -> ph ) )
35 34 2eximi 
 |-  ( E. z E. w A. x A. y ( ph <-> ( x = z /\ y = w ) ) -> E. z E. w A. x A. y ( ( x = z /\ y = w ) -> ph ) )
36 2exsb 
 |-  ( E. x E. y ph <-> E. z E. w A. x A. y ( ( x = z /\ y = w ) -> ph ) )
37 35 36 sylibr 
 |-  ( E. z E. w A. x A. y ( ph <-> ( x = z /\ y = w ) ) -> E. x E. y ph )
38 biimp 
 |-  ( ( ph <-> ( x = z /\ y = w ) ) -> ( ph -> ( x = z /\ y = w ) ) )
39 38 2alimi 
 |-  ( A. x A. y ( ph <-> ( x = z /\ y = w ) ) -> A. x A. y ( ph -> ( x = z /\ y = w ) ) )
40 39 2eximi 
 |-  ( E. z E. w A. x A. y ( ph <-> ( x = z /\ y = w ) ) -> E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) )
41 37 40 jca 
 |-  ( E. z E. w A. x A. y ( ph <-> ( x = z /\ y = w ) ) -> ( E. x E. y ph /\ E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )
42 32 41 impbii 
 |-  ( ( E. x E. y ph /\ E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) <-> E. z E. w A. x A. y ( ph <-> ( x = z /\ y = w ) ) )
43 1 42 bitri 
 |-  ( ( E! x E. y ph /\ E! y E. x ph ) <-> E. z E. w A. x A. y ( ph <-> ( x = z /\ y = w ) ) )