Metamath Proof Explorer

Theorem dfeumo

Description: An elementary proof showing the reverse direction of dfmoeu . Here the characterizing expression of existential uniqueness ( eu6 ) is derived from that of uniqueness ( df-mo ). (Contributed by Wolf Lammen, 3-Oct-2023)

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

Proof

Step Hyp Ref Expression
1 ax6ev ⊢ ∃ x x = y
2 biimpr ⊢ φ ↔ x = y → x = y → φ
3 2 aleximi ⊢ ∀ x φ ↔ x = y → ∃ x x = y → ∃ x φ
4 1 3 mpi ⊢ ∀ x φ ↔ x = y → ∃ x φ
5 4 exlimiv ⊢ ∃ y ∀ x φ ↔ x = y → ∃ x φ
6 5 pm4.71ri ⊢ ∃ y ∀ x φ ↔ x = y ↔ ∃ x φ ∧ ∃ y ∀ x φ ↔ x = y
7 abai ⊢ ∃ x φ ∧ ∃ y ∀ x φ ↔ x = y ↔ ∃ x φ ∧ ∃ x φ → ∃ y ∀ x φ ↔ x = y
8 dfmoeu ⊢ ∃ x φ → ∃ y ∀ x φ ↔ x = y ↔ ∃ y ∀ x φ → x = y
9 8 anbi2i ⊢ ∃ x φ ∧ ∃ x φ → ∃ y ∀ x φ ↔ x = y ↔ ∃ x φ ∧ ∃ y ∀ x φ → x = y
10 6 7 9 3bitrri ⊢ ∃ x φ ∧ ∃ y ∀ x φ → x = y ↔ ∃ y ∀ x φ ↔ x = y