![]() |
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 4151 | . . 3 ⊢ ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑦 ∣ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥)} | |
2 | brun 4976 | . . . . . 6 ⊢ (𝑦(𝐴 ∪ 𝐵)𝑥 ↔ (𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥)) | |
3 | 2 | exbii 1811 | . . . . 5 ⊢ (∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥 ↔ ∃𝑥(𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥)) |
4 | 19.43 1846 | . . . . 5 ⊢ (∃𝑥(𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥) ↔ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥)) | |
5 | 3, 4 | bitr2i 268 | . . . 4 ⊢ ((∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥) ↔ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥) |
6 | 5 | abbii 2837 | . . 3 ⊢ {𝑦 ∣ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥)} = {𝑦 ∣ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥} |
7 | 1, 6 | eqtri 2795 | . 2 ⊢ ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑦 ∣ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥} |
8 | df-dm 5413 | . . 3 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} | |
9 | df-dm 5413 | . . 3 ⊢ dom 𝐵 = {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥} | |
10 | 8, 9 | uneq12i 4019 | . 2 ⊢ (dom 𝐴 ∪ dom 𝐵) = ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) |
11 | df-dm 5413 | . 2 ⊢ dom (𝐴 ∪ 𝐵) = {𝑦 ∣ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥} | |
12 | 7, 10, 11 | 3eqtr4ri 2806 | 1 ⊢ dom (𝐴 ∪ 𝐵) = (dom 𝐴 ∪ dom 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∨ wo 834 = wceq 1508 ∃wex 1743 {cab 2751 ∪ cun 3820 class class class wbr 4925 dom cdm 5403 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-ext 2743 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-clab 2752 df-cleq 2764 df-clel 2839 df-nfc 2911 df-v 3410 df-un 3827 df-br 4926 df-dm 5413 |
This theorem is referenced by: rnun 5841 dmpropg 5908 dmtpop 5911 fntpg 6244 fnun 6293 wfrlem13 7769 wfrlem16 7772 tfrlem10 7825 sbthlem5 8425 fodomr 8462 axdc3lem4 9671 hashfun 13609 s4dom 14141 dmtrclfv 14237 setsdm 16371 strleun 16445 xpsfrnel2cda 16698 estrreslem2 17258 mvdco 18346 gsumzaddlem 18806 cnfldfun 20274 uhgrun 26577 upgrun 26621 umgrun 26623 vtxdun 26981 wlkp1 27184 eupthp1 27761 bnj1416 31988 fmlasuc0 32231 frrlem14 32694 noextend 32731 noextendseq 32732 nosupbday 32763 nosupbnd1 32772 nosupbnd2 32774 noetalem3 32777 noetalem4 32778 fixun 32928 rclexi 39376 rtrclex 39378 rtrclexi 39382 cnvrcl0 39386 dmtrcl 39388 dfrtrcl5 39390 dfrcl2 39420 dmtrclfvRP 39476 |
Copyright terms: Public domain | W3C validator |