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 5101	. . . . 5 ⊢ (𝑦 = 𝑧 → (𝑦𝐴𝑥 ↔ 𝑧𝐴𝑥))
2	1	exbidv 1922	. . . 4 ⊢ (𝑦 = 𝑧 → (∃𝑥 𝑦𝐴𝑥 ↔ ∃𝑥 𝑧𝐴𝑥))
3		breq1 5101	. . . . 5 ⊢ (𝑦 = 𝑧 → (𝑦𝐵𝑥 ↔ 𝑧𝐵𝑥))
4	3	exbidv 1922	. . . 4 ⊢ (𝑦 = 𝑧 → (∃𝑥 𝑦𝐵𝑥 ↔ ∃𝑥 𝑧𝐵𝑥))
5	2, 4	unabw 4259	. . 3 ⊢ ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑧 ∣ (∃𝑥 𝑧𝐴𝑥 ∨ ∃𝑥 𝑧𝐵𝑥)}
6		brun 5149	. . . . . 6 ⊢ (𝑧(𝐴 ∪ 𝐵)𝑥 ↔ (𝑧𝐴𝑥 ∨ 𝑧𝐵𝑥))
7	6	exbii 1849	. . . . 5 ⊢ (∃𝑥 𝑧(𝐴 ∪ 𝐵)𝑥 ↔ ∃𝑥(𝑧𝐴𝑥 ∨ 𝑧𝐵𝑥))
8		19.43 1883	. . . . 5 ⊢ (∃𝑥(𝑧𝐴𝑥 ∨ 𝑧𝐵𝑥) ↔ (∃𝑥 𝑧𝐴𝑥 ∨ ∃𝑥 𝑧𝐵𝑥))
9	7, 8	bitr2i 276	. . . 4 ⊢ ((∃𝑥 𝑧𝐴𝑥 ∨ ∃𝑥 𝑧𝐵𝑥) ↔ ∃𝑥 𝑧(𝐴 ∪ 𝐵)𝑥)
10	9	abbii 2803	. . 3 ⊢ {𝑧 ∣ (∃𝑥 𝑧𝐴𝑥 ∨ ∃𝑥 𝑧𝐵𝑥)} = {𝑧 ∣ ∃𝑥 𝑧(𝐴 ∪ 𝐵)𝑥}
11	5, 10	eqtri 2759	. 2 ⊢ ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑧 ∣ ∃𝑥 𝑧(𝐴 ∪ 𝐵)𝑥}
12		df-dm 5634	. . 3 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑥 𝑦𝐴𝑥}
13		df-dm 5634	. . 3 ⊢ dom 𝐵 = {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}
14	12, 13	uneq12i 4118	. 2 ⊢ (dom 𝐴 ∪ dom 𝐵) = ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥})
15		df-dm 5634	. 2 ⊢ dom (𝐴 ∪ 𝐵) = {𝑧 ∣ ∃𝑥 𝑧(𝐴 ∪ 𝐵)𝑥}
16	11, 14, 15	3eqtr4ri 2770	1 ⊢ dom (𝐴 ∪ 𝐵) = (dom 𝐴 ∪ dom 𝐵)

Syntax hints:   ∨ wo 847   = wceq 1541  ∃wex 1780  {cab 2714   ∪ cun 3899   class class class wbr 5098  dom cdm 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-dm 5634

This theorem is referenced by:  rnun  6103  dmpropg  6173  dmtpop  6176  fntpg  6552  fnun  6606  frrlem14  8241  tfrlem10  8318  sbthlem5  9019  fodomr  9056  fodomfir  9228  axdc3lem4  10363  hashfun  14360  s4dom  14842  dmtrclfv  14941  strleun  17084  setsdm  17097  estrreslem2  18061  mvdco  19374  gsumzaddlem  19850  cnfldfunALT  21324  cnfldfunALTOLD  21337  noextend  27634  noextendseq  27635  nosupbday  27673  nosupbnd1  27682  nosupbnd2  27684  noinfbday  27688  noinfbnd1  27697  noinfbnd2  27699  noetasuplem4  27704  noetainflem4  27708  uhgrun  29147  upgrun  29191  umgrun  29193  vtxdun  29555  wlkp1  29753  eupthp1  30291  bnj1416  35195  fineqvac  35272  satfdm  35563  fmlasuc0  35578  fixun  36101  dmuncnvepres  38576  dfsucmap3  38637  rclexi  43856  rtrclex  43858  rtrclexi  43862  cnvrcl0  43866  dmtrcl  43868  dfrtrcl5  43870  dfrcl2  43915  dmtrclfvRP  43971