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

Metamath Proof Explorer

Theorem eu6im

Description: One direction of eu6 needs fewer axioms. (Contributed by Wolf Lammen, 2-Mar-2023)

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

Proof

Step Hyp Ref Expression
1 exsbim ⊢ ∃ y ∀ x x = y → φ → ∃ x φ
2 1 anim1i ⊢ ∃ y ∀ x x = y → φ ∧ ∃ z ∀ x φ → x = z → ∃ x φ ∧ ∃ z ∀ x φ → x = z
3 eu6lem ⊢ ∃ y ∀ x φ ↔ x = y ↔ ∃ y ∀ x x = y → φ ∧ ∃ z ∀ x φ → x = z
4 eu3v ⊢ ∃! x φ ↔ ∃ x φ ∧ ∃ z ∀ x φ → x = z
5 2 3 4 3imtr4i ⊢ ∃ y ∀ x φ ↔ x = y → ∃! x φ