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

Metamath Proof Explorer

Theorem idsymrel

Description: The identity relation is symmetric. (Contributed by AV, 19-Jun-2022)

Ref Expression
Assertion idsymrel ⊢ SymRel I

Proof

Step Hyp Ref Expression
1 cnvi ⊢ I -1 = I
2 reli ⊢ Rel ⁡ I
3 dfsymrel4 ⊢ SymRel I ↔ I -1 = I ∧ Rel ⁡ I
4 1 2 3 mpbir2an ⊢ SymRel I