Theorem dmun 5859

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.)

Assertion

Ref	Expression
dmun	⊢ dom (𝐴 ∪ 𝐵) = (dom 𝐴 ∪ dom 𝐵)

Proof of Theorem dmun

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq1 5082	. . . . 5 ⊢ (𝑦 = 𝑧 → (𝑦𝐴𝑥 ↔ 𝑧𝐴𝑥))
2	1	exbidv 1928	. . . 4 ⊢ (𝑦 = 𝑧 → (∃𝑥 𝑦𝐴𝑥 ↔ ∃𝑥 𝑧𝐴𝑥))
3		breq1 5082	. . . . 5 ⊢ (𝑦 = 𝑧 → (𝑦𝐵𝑥 ↔ 𝑧𝐵𝑥))
4	3	exbidv 1928	. . . 4 ⊢ (𝑦 = 𝑧 → (∃𝑥 𝑦𝐵𝑥 ↔ ∃𝑥 𝑧𝐵𝑥))
5	2, 4	unabw 4242	. . 3 ⊢ ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑧 ∣ (∃𝑥 𝑧𝐴𝑥 ∨ ∃𝑥 𝑧𝐵𝑥)}
6		brun 5130	. . . . . 6 ⊢ (𝑧(𝐴 ∪ 𝐵)𝑥 ↔ (𝑧𝐴𝑥 ∨ 𝑧𝐵𝑥))
7	6	exbii 1855	. . . . 5 ⊢ (∃𝑥 𝑧(𝐴 ∪ 𝐵)𝑥 ↔ ∃𝑥(𝑧𝐴𝑥 ∨ 𝑧𝐵𝑥))
8		19.43 1889	. . . . 5 ⊢ (∃𝑥(𝑧𝐴𝑥 ∨ 𝑧𝐵𝑥) ↔ (∃𝑥 𝑧𝐴𝑥 ∨ ∃𝑥 𝑧𝐵𝑥))
9	7, 8	bitr2i 277	. . . 4 ⊢ ((∃𝑥 𝑧𝐴𝑥 ∨ ∃𝑥 𝑧𝐵𝑥) ↔ ∃𝑥 𝑧(𝐴 ∪ 𝐵)𝑥)
10	9	abbii 2807	. . 3 ⊢ {𝑧 ∣ (∃𝑥 𝑧𝐴𝑥 ∨ ∃𝑥 𝑧𝐵𝑥)} = {𝑧 ∣ ∃𝑥 𝑧(𝐴 ∪ 𝐵)𝑥}
11	5, 10	eqtri 2763	. 2 ⊢ ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑧 ∣ ∃𝑥 𝑧(𝐴 ∪ 𝐵)𝑥}
12		df-dm 5635	. . 3 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑥 𝑦𝐴𝑥}
13		df-dm 5635	. . 3 ⊢ dom 𝐵 = {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}
14	12, 13	uneq12i 4103	. 2 ⊢ (dom 𝐴 ∪ dom 𝐵) = ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥})
15		df-dm 5635	. 2 ⊢ dom (𝐴 ∪ 𝐵) = {𝑧 ∣ ∃𝑥 𝑧(𝐴 ∪ 𝐵)𝑥}
16	11, 14, 15	3eqtr4ri 2774	1 ⊢ dom (𝐴 ∪ 𝐵) = (dom 𝐴 ∪ dom 𝐵)

Syntax hints:   ∨ wo 853   = wceq 1547  ∃wex 1786  {cab 2718   ∪ cun 3888   class class class wbr 5079  dom cdm 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-dm 5635

This theorem is referenced by:  rnun  6103  dmpropg  6173  dmtpop  6176  fntpg  6552  fnun  6606  frrlem14  8246  tfrlem10  8323  sbthlem5  9026  fodomr  9063  fodomfir  9235  axdc3lem4  10373  hashfun  14397  s4dom  14879  dmtrclfv  14978  strleun  17125  setsdm  17138  estrreslem2  18102  mvdco  19418  gsumzaddlem  19894  cnfldfunALT  21369  noextend  27655  noextendseq  27656  nosupbday  27694  nosupbnd1  27703  nosupbnd2  27705  noinfbday  27709  noinfbnd1  27718  noinfbnd2  27720  noetasuplem4  27725  noetainflem4  27729  uhgrun  29168  upgrun  29212  umgrun  29214  vtxdun  29575  wlkp1  29773  eupthp1  30311  bnj1416  35228  fineqvac  35304  satfdm  35604  fmlasuc0  35619  fixun  36142  dmuncnvepres  38765  dfsucmap3  38837  rclexi  44066  rtrclex  44068  rtrclexi  44072  cnvrcl0  44076  dmtrcl  44078  dfrtrcl5  44080  dfrcl2  44125  dmtrclfvRP  44181