This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dmcoels

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 = ⋃ A

Proof

Step Hyp Ref Expression
1 df-coels ⊢ ∼ A = ≀ E -1 ↾ A
2 1 dmeqi ⊢ dom ⁡ ∼ A = dom ⁡ ≀ E -1 ↾ A
3 dm1cosscnvepres ⊢ dom ⁡ ≀ E -1 ↾ A = ⋃ A
4 2 3 eqtri ⊢ dom ⁡ ∼ A = ⋃ A