Theorem elid

Description: Characterization of the elements of the identity relation. TODO: reorder theorems to move this theorem and dfrel3 after elrid . (Contributed by BJ, 28-Aug-2022)

	Ref	Expression
Assertion	elid	$$⊢A\in \mathrm{I}\leftrightarrow \exists xA=⟨x,x⟩$$

Proof

Step	Hyp	Ref	Expression
1		reli	$$⊢\mathrm{Rel}\mathrm{I}$$
2		dfrel3	$$⊢\mathrm{Rel}\mathrm{I}\leftrightarrow {\mathrm{I}\upharpoonright }_{\mathrm{V}}=\mathrm{I}$$
3	1 2	mpbi	$$⊢{\mathrm{I}\upharpoonright }_{\mathrm{V}}=\mathrm{I}$$
4	3	eqcomi	$$⊢\mathrm{I}={\mathrm{I}\upharpoonright }_{\mathrm{V}}$$
5	4	eleq2i	$$⊢A\in \mathrm{I}\leftrightarrow A\in \left({\mathrm{I}\upharpoonright }_{\mathrm{V}}\right)$$
6		elrid	$$⊢A\in \left({\mathrm{I}\upharpoonright }_{\mathrm{V}}\right)\leftrightarrow \exists x\in \mathrm{V}A=⟨x,x⟩$$
7		rexv	$$⊢\exists x\in \mathrm{V}A=⟨x,x⟩\leftrightarrow \exists xA=⟨x,x⟩$$
8	5 6 7	3bitri	$$⊢A\in \mathrm{I}\leftrightarrow \exists xA=⟨x,x⟩$$