Metamath Proof Explorer

Theorem dmun

Description: The domain of a union is the union of domains. Exercise 56(a) of Enderton p. 65. (Contributed by NM, 12-Aug-1994) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion dmun ⊢ dom ⁡ A ∪ B = dom ⁡ A ∪ dom ⁡ B

Proof

Step Hyp Ref Expression
1 breq1 ⊢ y = z → y A x ↔ z A x
2 1 exbidv ⊢ y = z → ∃ x y A x ↔ ∃ x z A x
3 breq1 ⊢ y = z → y B x ↔ z B x
4 3 exbidv ⊢ y = z → ∃ x y B x ↔ ∃ x z B x
5 2 4 unabw ⊢ y | ∃ x y A x ∪ y | ∃ x y B x = z | ∃ x z A x ∨ ∃ x z B x
6 brun ⊢ z A ∪ B x ↔ z A x ∨ z B x
7 6 exbii ⊢ ∃ x z A ∪ B x ↔ ∃ x z A x ∨ z B x
8 19.43 ⊢ ∃ x z A x ∨ z B x ↔ ∃ x z A x ∨ ∃ x z B x
9 7 8 bitr2i ⊢ ∃ x z A x ∨ ∃ x z B x ↔ ∃ x z A ∪ B x
10 9 abbii ⊢ z | ∃ x z A x ∨ ∃ x z B x = z | ∃ x z A ∪ B x
11 5 10 eqtri ⊢ y | ∃ x y A x ∪ y | ∃ x y B x = z | ∃ x z A ∪ B x
12 df-dm ⊢ dom ⁡ A = y | ∃ x y A x
13 df-dm ⊢ dom ⁡ B = y | ∃ x y B x
14 12 13 uneq12i ⊢ dom ⁡ A ∪ dom ⁡ B = y | ∃ x y A x ∪ y | ∃ x y B x
15 df-dm ⊢ dom ⁡ A ∪ B = z | ∃ x z A ∪ B x
16 11 14 15 3eqtr4ri ⊢ dom ⁡ A ∪ B = dom ⁡ A ∪ dom ⁡ B