Description: Define the class of coelements on the class A , see also the alternate definition dfcoels . Possible definitions are the special cases of dfcoss3 and dfcoss4 . (Contributed by Peter Mazsa, 20-Nov-2019)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-coels | |- ~ A = ,~ ( `' _E |` A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cA | |- A |
|
| 1 | 0 | ccoels | |- ~ A |
| 2 | cep | |- _E |
|
| 3 | 2 | ccnv | |- `' _E |
| 4 | 3 0 | cres | |- ( `' _E |` A ) |
| 5 | 4 | ccoss | |- ,~ ( `' _E |` A ) |
| 6 | 1 5 | wceq | |- ~ A = ,~ ( `' _E |` A ) |