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 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 ) } )