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 ( ( ∃ 𝑥 𝜑 → ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )

Proof

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