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 ψ