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\in V\to \left(⟨A,A⟩\in \left({\mathrm{I}\upharpoonright }_B\right)\leftrightarrow A\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		ididg	$$⊢A\in V\to A\mathrm{I}A$$
2		df-br	$$⊢A\mathrm{I}A\leftrightarrow ⟨A,A⟩\in \mathrm{I}$$
3	1 2	sylib	$$⊢A\in V\to ⟨A,A⟩\in \mathrm{I}$$
4		opelres	$$⊢A\in V\to \left(⟨A,A⟩\in \left({\mathrm{I}\upharpoonright }_B\right)\leftrightarrow \left(A\in B\wedge ⟨A,A⟩\in \mathrm{I}\right)\right)$$
5	3 4	mpbiran2d	$$⊢A\in V\to \left(⟨A,A⟩\in \left({\mathrm{I}\upharpoonright }_B\right)\leftrightarrow A\in B\right)$$