Metamath Proof Explorer

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 ⊢ R ErALTV A → CoElEqvRel A ∧ ¬ ∅ ∈ A

Proof

Step Hyp Ref Expression
1 fences2 ⊢ R ErALTV A → ElDisj A ∧ ¬ ∅ ∈ A
2 eldisjim ⊢ ElDisj A → CoElEqvRel A
3 2 anim1i ⊢ ElDisj A ∧ ¬ ∅ ∈ A → CoElEqvRel A ∧ ¬ ∅ ∈ A
4 1 3 syl ⊢ R ErALTV A → CoElEqvRel A ∧ ¬ ∅ ∈ A