Description: Define the coelement equivalence relation predicate. (Read: the coelement equivalence relation on A .) Alternate definition is dfcoeleqvrel . For sets, being an element of the class of coelement equivalence relations is equivalent to satisfying the coelement equivalence relation predicate, see elcoeleqvrelsrel . (Contributed by Peter Mazsa, 11-Dec-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-coeleqvrel | |- ( CoElEqvRel A <-> EqvRel ,~ ( `' _E |` A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cA | |- A |
|
| 1 | 0 | wcoeleqvrel | |- CoElEqvRel A |
| 2 | cep | |- _E |
|
| 3 | 2 | ccnv | |- `' _E |
| 4 | 3 0 | cres | |- ( `' _E |` A ) |
| 5 | 4 | ccoss | |- ,~ ( `' _E |` A ) |
| 6 | 5 | weqvrel | |- EqvRel ,~ ( `' _E |` A ) |
| 7 | 1 6 | wb | |- ( CoElEqvRel A <-> EqvRel ,~ ( `' _E |` A ) ) |