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	⊢ ( 𝑅 ErALTV 𝐴 → ( CoElEqvRel 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		fences2	⊢ ( 𝑅 ErALTV 𝐴 → ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) )
2		eldisjim	⊢ ( ElDisj 𝐴 → CoElEqvRel 𝐴 )
3	2	anim1i	⊢ ( ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) → ( CoElEqvRel 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) )
4	1 3	syl	⊢ ( 𝑅 ErALTV 𝐴 → ( CoElEqvRel 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) )