Theorem mainer2

Description: The Main Theorem of Equivalences: every equivalence relation implies equivalent comembers. (Contributed by Peter Mazsa, 15-Oct-2021)

	Ref	Expression
Assertion	mainer2	$$⊢RErALTVA\to \left(CoElEqvRelA\wedge \neg \varnothing \in A\right)$$

Proof

Step	Hyp	Ref	Expression
1		fences2	$$⊢RErALTVA\to \left(ElDisjA\wedge \neg \varnothing \in A\right)$$
2		eldisjim	$$⊢ElDisjA\to CoElEqvRelA$$
3	2	anim1i	$$⊢\left(ElDisjA\wedge \neg \varnothing \in A\right)\to \left(CoElEqvRelA\wedge \neg \varnothing \in A\right)$$
4	1 3	syl	$$⊢RErALTVA\to \left(CoElEqvRelA\wedge \neg \varnothing \in A\right)$$