This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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