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 e. V -> ( A e. CoElEqvRels <-> ,~ ( `' _E |` A ) e. EqvRels ) )

Proof

Step Hyp Ref Expression
1 reseq2
 |-  ( a = A -> ( `' _E |` a ) = ( `' _E |` A ) )
2 1 cosseqd
 |-  ( a = A -> ,~ ( `' _E |` a ) = ,~ ( `' _E |` A ) )
3 2 eleq1d
 |-  ( a = A -> ( ,~ ( `' _E |` a ) e. EqvRels <-> ,~ ( `' _E |` A ) e. EqvRels ) )
4 df-coeleqvrels
 |-  CoElEqvRels = { a | ,~ ( `' _E |` a ) e. EqvRels }
5 3 4 elab2g
 |-  ( A e. V -> ( A e. CoElEqvRels <-> ,~ ( `' _E |` A ) e. EqvRels ) )