Metamath Proof Explorer


Theorem elcoeleqvrels

Description: Elementhood in the coelement equivalence relations class. (Contributed by Peter Mazsa, 24-Jul-2023)

Ref Expression
Assertion elcoeleqvrels A V A CoElEqvRels E -1 A EqvRels

Proof

Step Hyp Ref Expression
1 reseq2 a = A E -1 a = E -1 A
2 1 cosseqd a = A E -1 a = E -1 A
3 2 eleq1d a = A E -1 a EqvRels E -1 A EqvRels
4 df-coeleqvrels CoElEqvRels = a | E -1 a EqvRels
5 3 4 elab2g A V A CoElEqvRels E -1 A EqvRels