Theorem mainerim

Description: Every equivalence relation implies equivalent coelements. (Contributed by Peter Mazsa, 20-Oct-2021)

	Ref	Expression
Assertion	mainerim	$$⊢RErALTVA\to CoElEqvRelA$$

Proof

Step	Hyp	Ref	Expression
1		mainer2	$$⊢RErALTVA\to \left(CoElEqvRelA\wedge \neg \varnothing \in A\right)$$
2	1	simpld	$$⊢RErALTVA\to CoElEqvRelA$$