Theorem opelidres

Description: <. A , A >. belongs to a restriction of the identity class iff A belongs to the restricting class. (Contributed by FL, 27-Oct-2008) (Revised by NM, 30-Mar-2016)

	Ref	Expression
Assertion	opelidres	|- ( A e. V -> ( <. A , A >. e. ( _I |` B ) <-> A e. B ) )

Proof

Step	Hyp	Ref	Expression
1		ididg	|- ( A e. V -> A _I A )
2		df-br	|- ( A _I A <-> <. A , A >. e. _I )
3	1 2	sylib	|- ( A e. V -> <. A , A >. e. _I )
4		opelres	|- ( A e. V -> ( <. A , A >. e. ( _I |` B ) <-> ( A e. B /\ <. A , A >. e. _I ) ) )
5	3 4	mpbiran2d	|- ( A e. V -> ( <. A , A >. e. ( _I |` B ) <-> A e. B ) )