Theorem refrelid

Description: Identity relation is reflexive. (Contributed by Peter Mazsa, 25-Jul-2021)

	Ref	Expression
Assertion	refrelid	$$⊢RefRel\mathrm{I}$$

Proof

Step	Hyp	Ref	Expression
1		ssid	$$⊢\mathrm{I}\cap \left(\mathrm{dom}\mathrm{I}\times \mathrm{ran}\mathrm{I}\right)\subseteq \mathrm{I}\cap \left(\mathrm{dom}\mathrm{I}\times \mathrm{ran}\mathrm{I}\right)$$
2		reli	$$⊢\mathrm{Rel}\mathrm{I}$$
3		df-refrel	$$⊢RefRel\mathrm{I}\leftrightarrow \left(\mathrm{I}\cap \left(\mathrm{dom}\mathrm{I}\times \mathrm{ran}\mathrm{I}\right)\subseteq \mathrm{I}\cap \left(\mathrm{dom}\mathrm{I}\times \mathrm{ran}\mathrm{I}\right)\wedge \mathrm{Rel}\mathrm{I}\right)$$
4	1 2 3	mpbir2an	$$⊢RefRel\mathrm{I}$$