Metamath Proof Explorer

Theorem eqvrelcossid

Description: The cosets by the identity class are in equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2024)

Ref Expression
Assertion eqvrelcossid 
|- EqvRel ,~ _I

Proof

Step Hyp Ref Expression
1 disjALTVid 
 |-  Disj _I
2 1 disjimi 
 |-  EqvRel ,~ _I