Theorem refrelid

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

	Ref	Expression
Assertion	refrelid	⊢ RefRel I

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ ( I ∩ ( dom I × ran I ) ) ⊆ ( I ∩ ( dom I × ran I ) )
2		reli	⊢ Rel I
3		df-refrel	⊢ ( RefRel I ↔ ( ( I ∩ ( dom I × ran I ) ) ⊆ ( I ∩ ( dom I × ran I ) ) ∧ Rel I ) )
4	1 2 3	mpbir2an	⊢ RefRel I