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