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

Metamath Proof Explorer

Theorem dfmoeu

Description: An elementary proof of moeu in disguise, connecting an expression characterizing uniqueness ( df-mo ) to that of existential uniqueness ( eu6 ). No particular order of definition is required, as one can be derived from the other. This is shown here and in dfeumo . (Contributed by Wolf Lammen, 27-May-2019)

Ref Expression
Assertion dfmoeu ⊢ ∃ x φ → ∃ y ∀ x φ ↔ x = y ↔ ∃ y ∀ x φ → x = y

Proof

Step Hyp Ref Expression
1 alnex ⊢ ∀ x ¬ φ ↔ ¬ ∃ x φ
2 pm2.21 ⊢ ¬ φ → φ → x = y
3 2 alimi ⊢ ∀ x ¬ φ → ∀ x φ → x = y
4 1 3 sylbir ⊢ ¬ ∃ x φ → ∀ x φ → x = y
5 4 19.8ad ⊢ ¬ ∃ x φ → ∃ y ∀ x φ → x = y
6 biimp ⊢ φ ↔ x = y → φ → x = y
7 6 alimi ⊢ ∀ x φ ↔ x = y → ∀ x φ → x = y
8 7 eximi ⊢ ∃ y ∀ x φ ↔ x = y → ∃ y ∀ x φ → x = y
9 5 8 ja ⊢ ∃ x φ → ∃ y ∀ x φ ↔ x = y → ∃ y ∀ x φ → x = y
10 nfia1 ⊢ Ⅎ x ∀ x φ → x = y → ∀ x φ ↔ x = y
11 id ⊢ φ → φ
12 ax12v ⊢ x = y → φ → ∀ x x = y → φ
13 12 com12 ⊢ φ → x = y → ∀ x x = y → φ
14 11 13 embantd ⊢ φ → φ → x = y → ∀ x x = y → φ
15 14 spsd ⊢ φ → ∀ x φ → x = y → ∀ x x = y → φ
16 15 ancld ⊢ φ → ∀ x φ → x = y → ∀ x φ → x = y ∧ ∀ x x = y → φ
17 albiim ⊢ ∀ x φ ↔ x = y ↔ ∀ x φ → x = y ∧ ∀ x x = y → φ
18 16 17 imbitrrdi ⊢ φ → ∀ x φ → x = y → ∀ x φ ↔ x = y
19 10 18 exlimi ⊢ ∃ x φ → ∀ x φ → x = y → ∀ x φ ↔ x = y
20 19 eximdv ⊢ ∃ x φ → ∃ y ∀ x φ → x = y → ∃ y ∀ x φ ↔ x = y
21 20 com12 ⊢ ∃ y ∀ x φ → x = y → ∃ x φ → ∃ y ∀ x φ ↔ x = y
22 9 21 impbii ⊢ ∃ x φ → ∃ y ∀ x φ ↔ x = y ↔ ∃ y ∀ x φ → x = y