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 ⊢Ⅎyx=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φ→∀xx=z→∃yφ
10 8 9 syli ⊢∀yφ→x=z∧y=w→∃yφ→∀xx=z→∃yφ
11 10 com12 ⊢∃yφ→∀yφ→x=z∧y=w→∀xx=z→∃yφ
12 11 spsd ⊢∃yφ→∀x∀yφ→x=z∧y=w→∀xx=z→∃yφ
13 nfs1v ⊢Ⅎywyφ
14 simpr ⊢x=z∧y=w→y=w
15 14 imim2i ⊢φ→x=z∧y=w→φ→y=w
16 sbequ1 ⊢y=w→φ→wyφ
17 15 16 syli ⊢φ→x=z∧y=w→φ→wyφ
18 17 sps ⊢∀yφ→x=z∧y=w→φ→wyφ
19 3 13 18 exlimd ⊢∀yφ→x=z∧y=w→∃yφ→wyφ
20 19 imim2d ⊢∀yφ→x=z∧y=w→x=z→∃yφ→x=z→wyφ
21 20 al2imi ⊢∀x∀yφ→x=z∧y=w→∀xx=z→∃yφ→∀xx=z→wyφ
22 sb6 ⊢zxwyφ↔∀xx=z→wyφ
23 2sb6 ⊢zxwyφ↔∀x∀yx=z∧y=w→φ
24 22 23 bitr3i ⊢∀xx=z→wyφ↔∀x∀yx=z∧y=w→φ
25 21 24 imbitrdi ⊢∀x∀yφ→x=z∧y=w→∀xx=z→∃yφ→∀x∀yx=z∧y=w→φ
26 12 25 sylcom ⊢∃yφ→∀x∀yφ→x=z∧y=w→∀x∀yx=z∧y=w→φ
27 26 ancld ⊢∃yφ→∀x∀yφ→x=z∧y=w→∀x∀yφ→x=z∧y=w∧∀x∀yx=z∧y=w→φ
28 2albiim ⊢∀x∀yφ↔x=z∧y=w↔∀x∀yφ→x=z∧y=w∧∀x∀yx=z∧y=w→φ
29 27 28 imbitrrdi ⊢∃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∀yx=z∧y=w→φ
35 34 2eximi ⊢∃z∃w∀x∀yφ↔x=z∧y=w→∃z∃w∀x∀yx=z∧y=w→φ
36 2exsb ⊢∃x∃yφ↔∃z∃w∀x∀yx=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