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

Metamath Proof Explorer

Theorem rabeqsn

Description: Conditions for a restricted class abstraction to be a singleton. (Contributed by AV, 18-Apr-2019) (Proof shortened by AV, 26-Aug-2022)

Ref Expression
Assertion rabeqsn ⊢ x ∈ V | φ = X ↔ ∀ x x ∈ V ∧ φ ↔ x = X

Proof

Step Hyp Ref Expression
1 df-rab ⊢ x ∈ V | φ = x | x ∈ V ∧ φ
2 1 eqeq1i ⊢ x ∈ V | φ = X ↔ x | x ∈ V ∧ φ = X
3 absn ⊢ x | x ∈ V ∧ φ = X ↔ ∀ x x ∈ V ∧ φ ↔ x = X
4 2 3 bitri ⊢ x ∈ V | φ = X ↔ ∀ x x ∈ V ∧ φ ↔ x = X