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

Metamath Proof Explorer

Theorem rabsnel

Description: Truth implied by equality of a restricted class abstraction and a singleton. (Contributed by Thierry Arnoux, 15-Sep-2018)

Ref Expression
Hypothesis rabsnel.1 ⊢ B ∈ V
Assertion rabsnel ⊢ x ∈ A | φ = B → B ∈ A

Proof

Step Hyp Ref Expression
1 rabsnel.1 ⊢ B ∈ V
2 1 snid ⊢ B ∈ B
3 eleq2 ⊢ x ∈ A | φ = B → B ∈ x ∈ A | φ ↔ B ∈ B
4 2 3 mpbiri ⊢ x ∈ A | φ = B → B ∈ x ∈ A | φ
5 elrabi ⊢ B ∈ x ∈ A | φ → B ∈ A
6 4 5 syl ⊢ x ∈ A | φ = B → B ∈ A