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 4199 | . . 3 ⊢ ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑦 ∣ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥)} | |
2 | brun 5090 | . . . . . 6 ⊢ (𝑦(𝐴 ∪ 𝐵)𝑥 ↔ (𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥)) | |
3 | 2 | exbii 1855 | . . . . 5 ⊢ (∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥 ↔ ∃𝑥(𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥)) |
4 | 19.43 1890 | . . . . 5 ⊢ (∃𝑥(𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥) ↔ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥)) | |
5 | 3, 4 | bitr2i 279 | . . . 4 ⊢ ((∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥) ↔ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥) |
6 | 5 | abbii 2801 | . . 3 ⊢ {𝑦 ∣ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥)} = {𝑦 ∣ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥} |
7 | 1, 6 | eqtri 2759 | . 2 ⊢ ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑦 ∣ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥} |
8 | df-dm 5546 | . . 3 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} | |
9 | df-dm 5546 | . . 3 ⊢ dom 𝐵 = {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥} | |
10 | 8, 9 | uneq12i 4061 | . 2 ⊢ (dom 𝐴 ∪ dom 𝐵) = ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) |
11 | df-dm 5546 | . 2 ⊢ dom (𝐴 ∪ 𝐵) = {𝑦 ∣ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥} | |
12 | 7, 10, 11 | 3eqtr4ri 2770 | 1 ⊢ dom (𝐴 ∪ 𝐵) = (dom 𝐴 ∪ dom 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∨ wo 847 = wceq 1543 ∃wex 1787 {cab 2714 ∪ cun 3851 class class class wbr 5039 dom cdm 5536 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-10 2143 ax-12 2177 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-tru 1546 df-ex 1788 df-nf 1792 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-v 3400 df-un 3858 df-br 5040 df-dm 5546 |
This theorem is referenced by: rnun 5989 dmpropg 6058 dmtpop 6061 fntpg 6418 fnun 6468 frrlem14 8018 wfrlem13 8045 wfrlem16 8048 tfrlem10 8101 sbthlem5 8738 fodomr 8775 axdc3lem4 10032 hashfun 13969 s4dom 14449 dmtrclfv 14546 setsdm 16699 strleun 16775 estrreslem2 17599 mvdco 18791 gsumzaddlem 19260 cnfldfun 20329 uhgrun 27119 upgrun 27163 umgrun 27165 vtxdun 27523 wlkp1 27723 eupthp1 28253 bnj1416 32686 fineqvac 32733 satfdm 32998 fmlasuc0 33013 noextend 33555 noextendseq 33556 nosupbday 33594 nosupbnd1 33603 nosupbnd2 33605 noinfbday 33609 noinfbnd1 33618 noinfbnd2 33620 noetasuplem4 33625 noetainflem4 33629 fixun 33897 rclexi 40840 rtrclex 40842 rtrclexi 40846 cnvrcl0 40850 dmtrcl 40852 dfrtrcl5 40854 dfrcl2 40900 dmtrclfvRP 40956 |
Copyright terms: Public domain | W3C validator |