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 ⊢ ∃! x ∃ y φ ∧ ∃! y ∃ x φ ↔ ∃ z ∃ w ∀ x ∀ y φ ↔ x = z ∧ y = w

Proof

Step Hyp Ref Expression
1 2eu4 ⊢ ∃! x ∃ y φ ∧ ∃! y ∃ x φ ↔ ∃ x ∃ y φ ∧ ∃ z ∃ w ∀ x ∀ y φ → x = z ∧ y = w
2 nfia1 ⊢ Ⅎ x ∀ x ∀ y φ → x = z ∧ y = w → ∀ x ∀ y φ ↔ x = z ∧ y = w
3 nfa1 ⊢ Ⅎ y ∀ y φ → x = z ∧ y = w
4 nfv ⊢ Ⅎ y x = z
5 simpl ⊢ x = z ∧ y = w → x = z
6 5 imim2i ⊢ φ → x = z ∧ y = w → φ → x = z
7 6 sps ⊢ ∀ y φ → x = z ∧ y = w → φ → x = z
8 3 4 7 exlimd ⊢ ∀ y φ → x = z ∧ y = w → ∃ y φ → x = z
9 ax12v ⊢ x = z → ∃ y φ → ∀ x x = z → ∃ y φ
10 8 9 syli ⊢ ∀ y φ → x = z ∧ y = w → ∃ y φ → ∀ x x = z → ∃ y φ
11 10 com12 ⊢ ∃ y φ → ∀ y φ → x = z ∧ y = w → ∀ x x = z → ∃ y φ
12 11 spsd ⊢ ∃ y φ → ∀ x ∀ y φ → x = z ∧ y = w → ∀ x x = z → ∃ y φ
13 nfs1v ⊢ Ⅎ y w y φ
14 simpr ⊢ x = z ∧ y = w → y = w
15 14 imim2i ⊢ φ → x = z ∧ y = w → φ → y = w
16 sbequ1 ⊢ y = w → φ → w y φ
17 15 16 syli ⊢ φ → x = z ∧ y = w → φ → w y φ
18 17 sps ⊢ ∀ y φ → x = z ∧ y = w → φ → w y φ
19 3 13 18 exlimd ⊢ ∀ y φ → x = z ∧ y = w → ∃ y φ → w y φ
20 19 imim2d ⊢ ∀ y φ → x = z ∧ y = w → x = z → ∃ y φ → x = z → w y φ
21 20 al2imi ⊢ ∀ x ∀ y φ → x = z ∧ y = w → ∀ x x = z → ∃ y φ → ∀ x x = z → w y φ
22 sb6 ⊢ z x w y φ ↔ ∀ x x = z → w y φ
23 2sb6 ⊢ z x w y φ ↔ ∀ x ∀ y x = z ∧ y = w → φ
24 22 23 bitr3i ⊢ ∀ x x = z → w y φ ↔ ∀ x ∀ y x = z ∧ y = w → φ
25 21 24 syl6ib ⊢ ∀ x ∀ y φ → x = z ∧ y = w → ∀ x x = z → ∃ y φ → ∀ x ∀ y x = z ∧ y = w → φ
26 12 25 sylcom ⊢ ∃ y φ → ∀ x ∀ y φ → x = z ∧ y = w → ∀ x ∀ y x = z ∧ y = w → φ
27 26 ancld ⊢ ∃ y φ → ∀ x ∀ y φ → x = z ∧ y = w → ∀ x ∀ y φ → x = z ∧ y = w ∧ ∀ x ∀ y x = z ∧ y = w → φ
28 2albiim ⊢ ∀ x ∀ y φ ↔ x = z ∧ y = w ↔ ∀ x ∀ y φ → x = z ∧ y = w ∧ ∀ x ∀ y x = z ∧ y = w → φ
29 27 28 syl6ibr ⊢ ∃ y φ → ∀ x ∀ y φ → x = z ∧ y = w → ∀ x ∀ y φ ↔ x = z ∧ y = w
30 2 29 exlimi ⊢ ∃ x ∃ y φ → ∀ x ∀ y φ → x = z ∧ y = w → ∀ x ∀ y φ ↔ x = z ∧ y = w
31 30 2eximdv ⊢ ∃ x ∃ y φ → ∃ z ∃ w ∀ x ∀ y φ → x = z ∧ y = w → ∃ z ∃ w ∀ x ∀ y φ ↔ x = z ∧ y = w
32 31 imp ⊢ ∃ x ∃ y φ ∧ ∃ z ∃ w ∀ x ∀ y φ → x = z ∧ y = w → ∃ z ∃ w ∀ x ∀ y φ ↔ x = z ∧ y = w
33 biimpr ⊢ φ ↔ x = z ∧ y = w → x = z ∧ y = w → φ
34 33 2alimi ⊢ ∀ x ∀ y φ ↔ x = z ∧ y = w → ∀ x ∀ y x = z ∧ y = w → φ
35 34 2eximi ⊢ ∃ z ∃ w ∀ x ∀ y φ ↔ x = z ∧ y = w → ∃ z ∃ w ∀ x ∀ y x = z ∧ y = w → φ
36 2exsb ⊢ ∃ x ∃ y φ ↔ ∃ z ∃ w ∀ x ∀ y x = z ∧ y = w → φ
37 35 36 sylibr ⊢ ∃ z ∃ w ∀ x ∀ y φ ↔ x = z ∧ y = w → ∃ x ∃ y φ
38 biimp ⊢ φ ↔ x = z ∧ y = w → φ → x = z ∧ y = w
39 38 2alimi ⊢ ∀ x ∀ y φ ↔ x = z ∧ y = w → ∀ x ∀ y φ → x = z ∧ y = w
40 39 2eximi ⊢ ∃ z ∃ w ∀ x ∀ y φ ↔ x = z ∧ y = w → ∃ z ∃ w ∀ x ∀ y φ → x = z ∧ y = w
41 37 40 jca ⊢ ∃ z ∃ w ∀ x ∀ y φ ↔ x = z ∧ y = w → ∃ x ∃ y φ ∧ ∃ z ∃ w ∀ x ∀ y φ → x = z ∧ y = w
42 32 41 impbii ⊢ ∃ x ∃ y φ ∧ ∃ z ∃ w ∀ x ∀ y φ → x = z ∧ y = w ↔ ∃ z ∃ w ∀ x ∀ y φ ↔ x = z ∧ y = w
43 1 42 bitri ⊢ ∃! x ∃ y φ ∧ ∃! y ∃ x φ ↔ ∃ z ∃ w ∀ x ∀ y φ ↔ x = z ∧ y = w