Metamath Proof Explorer

Theorem mainerim

Description: Every equivalence relation implies equivalent coelements. (Contributed by Peter Mazsa, 20-Oct-2021)

Ref Expression
Assertion mainerim 
|- ( R ErALTV A -> CoElEqvRel A )

Proof

Step Hyp Ref Expression
1 mainer2 
 |-  ( R ErALTV A -> ( CoElEqvRel A /\ -. (/) e. A ) )
2 1 simpld 
 |-  ( R ErALTV A -> CoElEqvRel A )