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

Metamath Proof Explorer

Theorem euabsn2

Description: Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by Mario Carneiro, 14-Nov-2016)

Ref Expression
Assertion euabsn2 ⊢ ∃! x φ ↔ ∃ y x | φ = y

Proof

Step Hyp Ref Expression
1 eu6 ⊢ ∃! x φ ↔ ∃ y ∀ x φ ↔ x = y
2 absn ⊢ x | φ = y ↔ ∀ x φ ↔ x = y
3 2 exbii ⊢ ∃ y x | φ = y ↔ ∃ y ∀ x φ ↔ x = y
4 1 3 bitr4i ⊢ ∃! x φ ↔ ∃ y x | φ = y