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 ∅