Metamath Proof Explorer

Theorem eqvrelid

Description: The identity relation is an equivalence relation. (Contributed by Peter Mazsa, 15-Apr-2019) (Revised by Peter Mazsa, 31-Dec-2021)

Ref Expression
Assertion eqvrelid 
|- EqvRel _I

Proof

Step Hyp Ref Expression
1 disjALTVid 
 |-  Disj _I
2 1 disjimi 
 |-  EqvRel ,~ _I
3 cossid 
 |-  ,~ _I = _I
4 3 eqvreleqi 
 |-  ( EqvRel ,~ _I <-> EqvRel _I )
5 2 4 mpbi 
 |-  EqvRel _I