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