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

Metamath Proof Explorer

Theorem rabsneq

Description: Equality of class abstractions restricted to a singleton. (Contributed by AV, 17-May-2025)

Ref Expression
Assertion rabsneq ⊢ N ∈ V → x ∈ N | ψ = x ∈ V | x = N ∧ ψ

Proof

Step Hyp Ref Expression
1 velsn ⊢ x ∈ N ↔ x = N
2 eleq1a ⊢ N ∈ V → x = N → x ∈ V
3 2 pm4.71rd ⊢ N ∈ V → x = N ↔ x ∈ V ∧ x = N
4 1 3 bitrid ⊢ N ∈ V → x ∈ N ↔ x ∈ V ∧ x = N
5 4 anbi1d ⊢ N ∈ V → x ∈ N ∧ ψ ↔ x ∈ V ∧ x = N ∧ ψ
6 anass ⊢ x ∈ V ∧ x = N ∧ ψ ↔ x ∈ V ∧ x = N ∧ ψ
7 5 6 bitrdi ⊢ N ∈ V → x ∈ N ∧ ψ ↔ x ∈ V ∧ x = N ∧ ψ
8 7 abbidv ⊢ N ∈ V → x | x ∈ N ∧ ψ = x | x ∈ V ∧ x = N ∧ ψ
9 df-rab ⊢ x ∈ N | ψ = x | x ∈ N ∧ ψ
10 df-rab ⊢ x ∈ V | x = N ∧ ψ = x | x ∈ V ∧ x = N ∧ ψ
11 8 9 10 3eqtr4g ⊢ N ∈ V → x ∈ N | ψ = x ∈ V | x = N ∧ ψ