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

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 ( 𝐴 ∪ 𝐵 ) = ( dom 𝐴 ∪ dom 𝐵 )

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 𝐴 𝑥 ↔ 𝑧 𝐴 𝑥 ) )
2 1 exbidv ⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑥 𝑦 𝐴 𝑥 ↔ ∃ 𝑥 𝑧 𝐴 𝑥 ) )
3 breq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 𝐵 𝑥 ↔ 𝑧 𝐵 𝑥 ) )
4 3 exbidv ⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑥 𝑦 𝐵 𝑥 ↔ ∃ 𝑥 𝑧 𝐵 𝑥 ) )
5 2 4 unabw ⊢ ( { 𝑦 ∣ ∃ 𝑥 𝑦 𝐴 𝑥 } ∪ { 𝑦 ∣ ∃ 𝑥 𝑦 𝐵 𝑥 } ) = { 𝑧 ∣ ( ∃ 𝑥 𝑧 𝐴 𝑥 ∨ ∃ 𝑥 𝑧 𝐵 𝑥 ) }
6 brun ⊢ ( 𝑧 ( 𝐴 ∪ 𝐵 ) 𝑥 ↔ ( 𝑧 𝐴 𝑥 ∨ 𝑧 𝐵 𝑥 ) )
7 6 exbii ⊢ ( ∃ 𝑥 𝑧 ( 𝐴 ∪ 𝐵 ) 𝑥 ↔ ∃ 𝑥 ( 𝑧 𝐴 𝑥 ∨ 𝑧 𝐵 𝑥 ) )
8 19.43 ⊢ ( ∃ 𝑥 ( 𝑧 𝐴 𝑥 ∨ 𝑧 𝐵 𝑥 ) ↔ ( ∃ 𝑥 𝑧 𝐴 𝑥 ∨ ∃ 𝑥 𝑧 𝐵 𝑥 ) )
9 7 8 bitr2i ⊢ ( ( ∃ 𝑥 𝑧 𝐴 𝑥 ∨ ∃ 𝑥 𝑧 𝐵 𝑥 ) ↔ ∃ 𝑥 𝑧 ( 𝐴 ∪ 𝐵 ) 𝑥 )
10 9 abbii ⊢ { 𝑧 ∣ ( ∃ 𝑥 𝑧 𝐴 𝑥 ∨ ∃ 𝑥 𝑧 𝐵 𝑥 ) } = { 𝑧 ∣ ∃ 𝑥 𝑧 ( 𝐴 ∪ 𝐵 ) 𝑥 }
11 5 10 eqtri ⊢ ( { 𝑦 ∣ ∃ 𝑥 𝑦 𝐴 𝑥 } ∪ { 𝑦 ∣ ∃ 𝑥 𝑦 𝐵 𝑥 } ) = { 𝑧 ∣ ∃ 𝑥 𝑧 ( 𝐴 ∪ 𝐵 ) 𝑥 }
12 df-dm ⊢ dom 𝐴 = { 𝑦 ∣ ∃ 𝑥 𝑦 𝐴 𝑥 }
13 df-dm ⊢ dom 𝐵 = { 𝑦 ∣ ∃ 𝑥 𝑦 𝐵 𝑥 }
14 12 13 uneq12i ⊢ ( dom 𝐴 ∪ dom 𝐵 ) = ( { 𝑦 ∣ ∃ 𝑥 𝑦 𝐴 𝑥 } ∪ { 𝑦 ∣ ∃ 𝑥 𝑦 𝐵 𝑥 } )
15 df-dm ⊢ dom ( 𝐴 ∪ 𝐵 ) = { 𝑧 ∣ ∃ 𝑥 𝑧 ( 𝐴 ∪ 𝐵 ) 𝑥 }
16 11 14 15 3eqtr4ri ⊢ dom ( 𝐴 ∪ 𝐵 ) = ( dom 𝐴 ∪ dom 𝐵 )