Description: The domain of coelements in A is the union of A . (Contributed by Rodolfo Medina, 14-Oct-2010) (Revised by Peter Mazsa, 5-Apr-2018) (Revised by Peter Mazsa, 26-Sep-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | dmcoels | |- dom ~ A = U. A |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-coels | |- ~ A = ,~ ( `' _E |` A ) |
|
| 2 | 1 | dmeqi | |- dom ~ A = dom ,~ ( `' _E |` A ) |
| 3 | dm1cosscnvepres | |- dom ,~ ( `' _E |` A ) = U. A |
|
| 4 | 2 3 | eqtri | |- dom ~ A = U. A |