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 ) ) |
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 ) ) |