Theorem dmun 5891

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 5105	. . . . 5 ⊢ (𝑦 = 𝑧 → (𝑦𝐴𝑥 ↔ 𝑧𝐴𝑥))
2	1	exbidv 1953	. . . 4 ⊢ (𝑦 = 𝑧 → (∃𝑥 𝑦𝐴𝑥 ↔ ∃𝑥 𝑧𝐴𝑥))
3		breq1 5105	. . . . 5 ⊢ (𝑦 = 𝑧 → (𝑦𝐵𝑥 ↔ 𝑧𝐵𝑥))
4	3	exbidv 1953	. . . 4 ⊢ (𝑦 = 𝑧 → (∃𝑥 𝑦𝐵𝑥 ↔ ∃𝑥 𝑧𝐵𝑥))
5	2, 4	unabw 4252	. . 3 ⊢ ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑧 ∣ (∃𝑥 𝑧𝐴𝑥 ∨ ∃𝑥 𝑧𝐵𝑥)}
6		brun 5155	. . . . . 6 ⊢ (𝑧(𝐴 ∪ 𝐵)𝑥 ↔ (𝑧𝐴𝑥 ∨ 𝑧𝐵𝑥))
7	6	exbii 1880	. . . . 5 ⊢ (∃𝑥 𝑧(𝐴 ∪ 𝐵)𝑥 ↔ ∃𝑥(𝑧𝐴𝑥 ∨ 𝑧𝐵𝑥))
8		19.43 1914	. . . . 5 ⊢ (∃𝑥(𝑧𝐴𝑥 ∨ 𝑧𝐵𝑥) ↔ (∃𝑥 𝑧𝐴𝑥 ∨ ∃𝑥 𝑧𝐵𝑥))
9	7, 8	bitr2i 279	. . . 4 ⊢ ((∃𝑥 𝑧𝐴𝑥 ∨ ∃𝑥 𝑧𝐵𝑥) ↔ ∃𝑥 𝑧(𝐴 ∪ 𝐵)𝑥)
10	9	abbii 2827	. . 3 ⊢ {𝑧 ∣ (∃𝑥 𝑧𝐴𝑥 ∨ ∃𝑥 𝑧𝐵𝑥)} = {𝑧 ∣ ∃𝑥 𝑧(𝐴 ∪ 𝐵)𝑥}
11	5, 10	eqtri 2783	. 2 ⊢ ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑧 ∣ ∃𝑥 𝑧(𝐴 ∪ 𝐵)𝑥}
12		df-dm 5660	. . 3 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑥 𝑦𝐴𝑥}
13		df-dm 5660	. . 3 ⊢ dom 𝐵 = {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}
14	12, 13	uneq12i 4165	. 2 ⊢ (dom 𝐴 ∪ dom 𝐵) = ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥})
15		df-dm 5660	. 2 ⊢ dom (𝐴 ∪ 𝐵) = {𝑧 ∣ ∃𝑥 𝑧(𝐴 ∪ 𝐵)𝑥}
16	11, 14, 15	3eqtr4ri 2794	1 ⊢ dom (𝐴 ∪ 𝐵) = (dom 𝐴 ∪ dom 𝐵)

This proof depends on syntax axioms:   ∨ wo 861   = wceq 1569  ∃wex 1811  {cab 2738   ∪ cun 4149   class class class wbr 5102  dom cdm 5650

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-dm 5660

This theorem is used by:  rnun  6135  dmpropg  6216  dmtpop  6219  fntpg  6600  fnun  6653  frrlem14  8320  tfrlem10  8398  sbthlem5  9113  fodomr  9150  fodomfir  9322  axdc3lem4  10534  hashfun  14585  s4dom  15075  dmtrclfv  15176  strleun  17340  setsdm  17353  estrreslem2  18317  mvdco  19664  gsumzaddlem  20140  cnfldfunALT  21698  noextend  28028  noextendseq  28029  nosupbday  28067  nosupbnd1  28076  nosupbnd2  28078  noinfbday  28082  noinfbnd1  28091  noinfbnd2  28093  noetasuplem4  28098  noetainflem4  28102  uhgrun  29657  upgrun  29701  umgrun  29703  vtxdun  30067  wlkp1  30265  eupthp1  30822  bnj1416  35715  fineqvac  35840  satfdm  36220  fmlasuc0  36235  fixun  36763  dmuncnvepres  39416  dfsucmap3  39488  rclexi  44708  rtrclex  44710  rtrclexi  44714  cnvrcl0  44718  dmtrcl  44720  dfrtrcl5  44722  dfrcl2  44767  dmtrclfvRP  44823