Description: The identity relation is symmetric. (Contributed by AV, 19-Jun-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | idsymrel | ⊢ SymRel I |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnvi | ⊢ ◡ I = I | |
2 | reli | ⊢ Rel I | |
3 | dfsymrel4 | ⊢ ( SymRel I ↔ ( ◡ I = I ∧ Rel I ) ) | |
4 | 1 2 3 | mpbir2an | ⊢ SymRel I |