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 e. V -> { x e. { N } | ps } = { x e. V | ( x = N /\ ps ) } )

Proof

Step Hyp Ref Expression
1 velsn
 |-  ( x e. { N } <-> x = N )
2 eleq1a
 |-  ( N e. V -> ( x = N -> x e. V ) )
3 2 pm4.71rd
 |-  ( N e. V -> ( x = N <-> ( x e. V /\ x = N ) ) )
4 1 3 bitrid
 |-  ( N e. V -> ( x e. { N } <-> ( x e. V /\ x = N ) ) )
5 4 anbi1d
 |-  ( N e. V -> ( ( x e. { N } /\ ps ) <-> ( ( x e. V /\ x = N ) /\ ps ) ) )
6 anass
 |-  ( ( ( x e. V /\ x = N ) /\ ps ) <-> ( x e. V /\ ( x = N /\ ps ) ) )
7 5 6 bitrdi
 |-  ( N e. V -> ( ( x e. { N } /\ ps ) <-> ( x e. V /\ ( x = N /\ ps ) ) ) )
8 7 abbidv
 |-  ( N e. V -> { x | ( x e. { N } /\ ps ) } = { x | ( x e. V /\ ( x = N /\ ps ) ) } )
9 df-rab
 |-  { x e. { N } | ps } = { x | ( x e. { N } /\ ps ) }
10 df-rab
 |-  { x e. V | ( x = N /\ ps ) } = { x | ( x e. V /\ ( x = N /\ ps ) ) }
11 8 9 10 3eqtr4g
 |-  ( N e. V -> { x e. { N } | ps } = { x e. V | ( x = N /\ ps ) } )