Description: The domain of cosets of the restricted converse epsilon relation is the union of the restriction. (Contributed by Peter Mazsa, 18-May-2019) (Revised by Peter Mazsa, 26-Sep-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | dm1cosscnvepres | |- dom ,~ ( `' _E |` A ) = U. A |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dmcoss2 | |- dom ,~ ( `' _E |` A ) = ran ( `' _E |` A ) |
|
| 2 | rncnvepres | |- ran ( `' _E |` A ) = U. A |
|
| 3 | 1 2 | eqtri | |- dom ,~ ( `' _E |` A ) = U. A |