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

Metamath Proof Explorer

Theorem eueq

Description: A class is a set if and only if there exists a unique set equal to it. (Contributed by NM, 25-Nov-1994) Shorten combined proofs of moeq and eueq . (Proof shortened by BJ, 24-Sep-2022)

Ref Expression
Assertion eueq ⊢ A ∈ V ↔ ∃! x x = A

Proof

Step Hyp Ref Expression
1 moeq ⊢ ∃* x x = A
2 1 biantru ⊢ ∃ x x = A ↔ ∃ x x = A ∧ ∃* x x = A
3 isset ⊢ A ∈ V ↔ ∃ x x = A
4 df-eu ⊢ ∃! x x = A ↔ ∃ x x = A ∧ ∃* x x = A
5 2 3 4 3bitr4i ⊢ A ∈ V ↔ ∃! x x = A