Metamath Proof Explorer

Theorem eqvrel0

Description: The null class is an equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2021)

Ref Expression
Assertion eqvrel0 
|- EqvRel (/)

Proof

Step Hyp Ref Expression
1 disjALTV0 
 |-  Disj (/)
2 1 disjimi 
 |-  EqvRel ,~ (/)
3 coss0 
 |-  ,~ (/) = (/)
4 3 eqvreleqi 
 |-  ( EqvRel ,~ (/) <-> EqvRel (/) )
5 2 4 mpbi 
 |-  EqvRel (/)