Theorem ressn2

Description: A class ' R ' restricted to the singleton of the class ' A ' is the ordered pair class abstraction of the class ' A ' and the sets in relation ' R ' to ' A ' (and not in relation to the singleton ' { A } ' ). (Contributed by Peter Mazsa, 16-Jun-2024)

	Ref	Expression
Assertion	ressn2	|- ( R |` { A } ) = { <. a , u >. | ( a = A /\ A R u ) }

Proof

Step	Hyp	Ref	Expression
1		dfres2	|- ( R |` { A } ) = { <. a , u >. | ( a e. { A } /\ a R u ) }
2		velsn	|- ( a e. { A } <-> a = A )
3	2	anbi1i	|- ( ( a e. { A } /\ a R u ) <-> ( a = A /\ a R u ) )
4		eqbrb	|- ( ( a = A /\ a R u ) <-> ( a = A /\ A R u ) )
5	3 4	bitri	|- ( ( a e. { A } /\ a R u ) <-> ( a = A /\ A R u ) )
6	5	opabbii	|- { <. a , u >. | ( a e. { A } /\ a R u ) } = { <. a , u >. | ( a = A /\ A R u ) }
7	1 6	eqtri	|- ( R |` { A } ) = { <. a , u >. | ( a = A /\ A R u ) }