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 /\ -. (/) e. A ) )

Proof

Step Hyp Ref Expression
1 fences2 
 |-  ( R ErALTV A -> ( ElDisj A /\ -. (/) e. A ) )
2 eldisjim 
 |-  ( ElDisj A -> CoElEqvRel A )
3 2 anim1i 
 |-  ( ( ElDisj A /\ -. (/) e. A ) -> ( CoElEqvRel A /\ -. (/) e. A ) )
4 1 3 syl 
 |-  ( R ErALTV A -> ( CoElEqvRel A /\ -. (/) e. A ) )