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 = _I
2 reli 
 |-  Rel _I
3 dfsymrel4 
 |-  ( SymRel _I <-> ( `' _I = _I /\ Rel _I ) )
4 1 2 3 mpbir2an 
 |-  SymRel _I