![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dmun | Structured version Visualization version GIF version |
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 |
---|---|
dmun | ⊢ dom (𝐴 ∪ 𝐵) = (dom 𝐴 ∪ dom 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unab 4299 | . . 3 ⊢ ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑦 ∣ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥)} | |
2 | brun 5200 | . . . . . 6 ⊢ (𝑦(𝐴 ∪ 𝐵)𝑥 ↔ (𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥)) | |
3 | 2 | exbii 1851 | . . . . 5 ⊢ (∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥 ↔ ∃𝑥(𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥)) |
4 | 19.43 1886 | . . . . 5 ⊢ (∃𝑥(𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥) ↔ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥)) | |
5 | 3, 4 | bitr2i 276 | . . . 4 ⊢ ((∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥) ↔ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥) |
6 | 5 | abbii 2803 | . . 3 ⊢ {𝑦 ∣ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥)} = {𝑦 ∣ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥} |
7 | 1, 6 | eqtri 2761 | . 2 ⊢ ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑦 ∣ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥} |
8 | df-dm 5687 | . . 3 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} | |
9 | df-dm 5687 | . . 3 ⊢ dom 𝐵 = {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥} | |
10 | 8, 9 | uneq12i 4162 | . 2 ⊢ (dom 𝐴 ∪ dom 𝐵) = ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) |
11 | df-dm 5687 | . 2 ⊢ dom (𝐴 ∪ 𝐵) = {𝑦 ∣ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥} | |
12 | 7, 10, 11 | 3eqtr4ri 2772 | 1 ⊢ dom (𝐴 ∪ 𝐵) = (dom 𝐴 ∪ dom 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∨ wo 846 = wceq 1542 ∃wex 1782 {cab 2710 ∪ cun 3947 class class class wbr 5149 dom cdm 5677 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-12 2172 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-un 3954 df-br 5150 df-dm 5687 |
This theorem is referenced by: rnun 6146 dmpropg 6215 dmtpop 6218 fntpg 6609 fnun 6664 frrlem14 8284 wfrlem13OLD 8321 wfrlem16OLD 8324 tfrlem10 8387 sbthlem5 9087 fodomr 9128 axdc3lem4 10448 hashfun 14397 s4dom 14870 dmtrclfv 14965 strleun 17090 setsdm 17103 estrreslem2 18090 mvdco 19313 gsumzaddlem 19789 cnfldfunALT 20957 cnfldfunALTOLD 20958 noextend 27169 noextendseq 27170 nosupbday 27208 nosupbnd1 27217 nosupbnd2 27219 noinfbday 27223 noinfbnd1 27232 noinfbnd2 27234 noetasuplem4 27239 noetainflem4 27243 uhgrun 28334 upgrun 28378 umgrun 28380 vtxdun 28738 wlkp1 28938 eupthp1 29469 bnj1416 34050 fineqvac 34097 satfdm 34360 fmlasuc0 34375 fixun 34881 rclexi 42366 rtrclex 42368 rtrclexi 42372 cnvrcl0 42376 dmtrcl 42378 dfrtrcl5 42380 dfrcl2 42425 dmtrclfvRP 42481 |
Copyright terms: Public domain | W3C validator |