Theorem elrid

Description: Characterization of the elements of a restricted identity relation. (Contributed by BJ, 28-Aug-2022) (Proof shortened by Peter Mazsa, 9-Sep-2022)

	Ref	Expression
Assertion	elrid	$$⊢A\in \left({\mathrm{I}\upharpoonright }_X\right)\leftrightarrow \exists x\in XA=⟨x,x⟩$$

Proof

Step	Hyp	Ref	Expression
1		df-res	$$⊢{\mathrm{I}\upharpoonright }_X=\mathrm{I}\cap \left(X\times \mathrm{V}\right)$$
2	1	eleq2i	$$⊢A\in \left({\mathrm{I}\upharpoonright }_X\right)\leftrightarrow A\in \left(\mathrm{I}\cap \left(X\times \mathrm{V}\right)\right)$$
3		elidinxp	$$⊢A\in \left(\mathrm{I}\cap \left(X\times \mathrm{V}\right)\right)\leftrightarrow \exists x\in \left(X\cap \mathrm{V}\right)A=⟨x,x⟩$$
4		inv1	$$⊢X\cap \mathrm{V}=X$$
5	4	rexeqi	$$⊢\exists x\in \left(X\cap \mathrm{V}\right)A=⟨x,x⟩\leftrightarrow \exists x\in XA=⟨x,x⟩$$
6	2 3 5	3bitri	$$⊢A\in \left({\mathrm{I}\upharpoonright }_X\right)\leftrightarrow \exists x\in XA=⟨x,x⟩$$