Theorem opabresid

Description: The restricted identity relation expressed as an ordered-pair class abstraction. (Contributed by FL, 25-Apr-2012)

	Ref	Expression
Assertion	opabresid	|- ( _I |` A ) = { <. x , y >. | ( x e. A /\ y = x ) }

Proof

Step	Hyp	Ref	Expression
1		df-id	|- _I = { <. x , y >. | x = y }
2		equcom	|- ( x = y <-> y = x )
3	2	opabbii	|- { <. x , y >. | x = y } = { <. x , y >. | y = x }
4	1 3	eqtri	|- _I = { <. x , y >. | y = x }
5	4	reseq1i	|- ( _I |` A ) = ( { <. x , y >. | y = x } |` A )
6		resopab	|- ( { <. x , y >. | y = x } |` A ) = { <. x , y >. | ( x e. A /\ y = x ) }
7	5 6	eqtri	|- ( _I |` A ) = { <. x , y >. | ( x e. A /\ y = x ) }