Theorem unex 7738

Description: The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 1-Jul-1994.)

Hypotheses

Ref	Expression
unex.1	⊢ 𝐴 ∈ V
unex.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
unex	⊢ (𝐴 ∪ 𝐵) ∈ V

Proof of Theorem unex

Step	Hyp	Ref	Expression
1		unex.1	. 2 ⊢ 𝐴 ∈ V
2		unex.2	. 2 ⊢ 𝐵 ∈ V
3		unexg 7737	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∪ 𝐵) ∈ V)
4	1, 2, 3	mp2an 692	1 ⊢ (𝐴 ∪ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3459   ∪ cun 3924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7729

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-sn 4602  df-pr 4604  df-uni 4884

This theorem is referenced by:  tpex  7740  unexbOLD  7742  fvclex  7957  naddcllem  8688  ralxpmap  8910  unen  9060  undom  9073  enfixsn  9095  sbthlem10  9106  dif1en  9174  dif1enOLD  9176  findcard2  9178  unxpdomlem3  9260  isinf  9268  isinfOLD  9269  ac6sfi  9292  pwfilem  9328  cnfcomlem  9713  trcl  9742  tc2  9756  rankxpu  9890  rankxplim  9893  rankxplim3  9895  r0weon  10026  infxpenlem  10027  dfac4  10136  dfac2b  10145  kmlem2  10166  cfsmolem  10284  isfin1-3  10400  axdc2lem  10462  axdc3lem4  10467  axcclem  10471  ttukeylem3  10525  gchac  10695  wunex2  10752  wuncval2  10761  inar1  10789  nn0ex  12507  xrex  13003  seqexw  14035  hashbclem  14470  incexclem  15852  ramub1lem2  17047  prdsval  17469  imasval  17525  ipoval  18540  plusffval  18624  smndex1bas  18884  smndex1sgrp  18886  smndex1mnd  18888  smndex1id  18889  grpinvfval  18961  grpsubfval  18966  mulgfval  19052  staffval  20801  scaffval  20837  lpival  21285  cnfldex  21318  xrsex  21345  ipffval  21608  islindf4  21798  psrval  21875  neitr  23118  leordtval2  23150  comppfsc  23470  1stckgen  23492  dfac14  23556  ptcmpfi  23751  hausflim  23919  flimclslem  23922  alexsubALTlem2  23986  nmfval  24527  icccmplem2  24763  tcphex  25169  tchnmfval  25180  taylfval  26318  lrrecse  27901  addsval  27921  negsval  27983  negsid  27999  mulsval  28064  mulsproplem9  28079  precsexlem4  28164  precsexlem5  28165  onscutlt  28217  onaddscl  28226  legval  28563  axlowdimlem15  28935  axlowdim  28940  eengv  28958  uhgrunop  29054  upgrunop  29098  umgrunop  29100  padct  32697  cycpmconjslem2  33166  rlocbas  33262  rlocaddval  33263  rlocmulval  33264  idlsrgval  33518  ordtconnlem1  33955  sxbrsigalem2  34318  actfunsnf1o  34636  actfunsnrndisj  34637  reprsuc  34647  breprexplema  34662  bnj918  34797  fineqvac  35128  subfacp1lem3  35204  subfacp1lem5  35206  erdszelem8  35220  satfvsuclem1  35381  satf0suc  35398  fmlasuc0  35406  mrexval  35523  mrsubcv  35532  mrsubff  35534  mrsubccat  35540  elmrsubrn  35542  rdgssun  37396  exrecfnlem  37397  finixpnum  37629  poimirlem4  37648  poimirlem15  37659  poimirlem28  37672  rrnval  37851  lsatset  39008  ldualset  39143  pclfinN  39919  dvaset  41024  dvhset  41100  hlhilset  41953  evlselv  42610  elrfi  42717  istopclsd  42723  mzpcompact2lem  42774  eldioph2lem1  42783  eldioph2lem2  42784  eldioph4b  42834  diophren  42836  ttac  43060  pwslnmlem2  43117  dfacbasgrp  43132  mendval  43203  idomsubgmo  43217  superuncl  43592  ssuncl  43594  sssymdifcl  43596  rclexi  43639  trclexi  43644  rtrclexi  43645  dfrtrcl5  43653  dfrcl2  43698  comptiunov2i  43730  cotrclrcl  43766  frege83  43970  frege110  43997  frege133  44020  clsk1indlem3  44067  permaxinf2lem  45037  fnchoice  45053  limcresiooub  45671  limcresioolb  45672  fourierdlem48  46183  fourierdlem49  46184  fourierdlem102  46237  fourierdlem114  46249  sge0resplit  46435  elpglem2  49576