Theorem opabresidOLD

Description: Obsolete version of opabresid as of 26-Dec-2023. (Contributed by FL, 25-Apr-2012) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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