Theorem unex 7691

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 7690	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∪ 𝐵) ∈ V)
4	1, 2, 3	mp2an 693	1 ⊢ (𝐴 ∪ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3430   ∪ cun 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907  df-sn 4569  df-pr 4571  df-uni 4852

This theorem is referenced by:  tpex  7693  unexbOLD  7695  fvclex  7905  naddcllem  8605  ralxpmap  8837  unen  8985  undom  8996  enfixsn  9017  sbthlem10  9027  dif1en  9089  findcard2  9092  unxpdomlem3  9161  isinf  9168  ac6sfi  9187  pwfilem  9221  cnfcomlem  9611  trcl  9640  tc2  9652  rankxpu  9791  rankxplim  9794  rankxplim3  9796  r0weon  9925  infxpenlem  9926  dfac4  10035  dfac2b  10044  kmlem2  10065  cfsmolem  10183  isfin1-3  10299  axdc2lem  10361  axdc3lem4  10366  axcclem  10370  ttukeylem3  10424  gchac  10595  wunex2  10652  wuncval2  10661  inar1  10689  nn0ex  12434  xrex  12928  seqexw  13970  hashbclem  14405  incexclem  15792  ramub1lem2  16989  prdsval  17409  imasval  17466  ipoval  18487  plusffval  18605  smndex1bas  18868  smndex1sgrp  18870  smndex1mnd  18872  smndex1id  18873  grpinvfval  18945  grpsubfval  18950  mulgfval  19036  staffval  20809  scaffval  20866  lpival  21314  cnfldex  21347  xrsex  21374  ipffval  21638  islindf4  21828  psrval  21905  neitr  23155  leordtval2  23187  comppfsc  23507  1stckgen  23529  dfac14  23593  ptcmpfi  23788  hausflim  23956  flimclslem  23959  alexsubALTlem2  24023  nmfval  24563  icccmplem2  24799  tcphex  25194  tchnmfval  25205  taylfval  26335  lrrecse  27948  addsval  27968  negsval  28031  negsid  28047  mulsval  28115  mulsproplem9  28130  precsexlem4  28216  precsexlem5  28217  oncutlt  28270  onaddscl  28283  legval  28666  axlowdimlem15  29039  axlowdim  29044  eengv  29062  uhgrunop  29158  upgrunop  29202  umgrunop  29204  padct  32806  cycpmconjslem2  33231  rlocbas  33343  rlocaddval  33344  rlocmulval  33345  idlsrgval  33578  ordtconnlem1  34084  sxbrsigalem2  34446  actfunsnf1o  34764  actfunsnrndisj  34765  reprsuc  34775  breprexplema  34790  bnj918  34925  fineqvac  35276  subfacp1lem3  35380  subfacp1lem5  35382  erdszelem8  35396  satfvsuclem1  35557  satf0suc  35574  fmlasuc0  35582  mrexval  35699  mrsubcv  35708  mrsubff  35710  mrsubccat  35716  elmrsubrn  35718  dfttc4lem2  36727  rdgssun  37708  exrecfnlem  37709  finixpnum  37940  poimirlem4  37959  poimirlem15  37970  poimirlem28  37983  rrnval  38162  lsatset  39450  ldualset  39585  pclfinN  40360  dvaset  41465  dvhset  41541  hlhilset  42394  evlselv  43034  elrfi  43140  istopclsd  43146  mzpcompact2lem  43197  eldioph2lem1  43206  eldioph2lem2  43207  eldioph4b  43257  diophren  43259  ttac  43482  pwslnmlem2  43539  dfacbasgrp  43554  mendval  43625  idomsubgmo  43639  superuncl  44013  ssuncl  44015  sssymdifcl  44017  rclexi  44060  trclexi  44065  rtrclexi  44066  dfrtrcl5  44074  dfrcl2  44119  comptiunov2i  44151  cotrclrcl  44187  frege83  44391  frege110  44418  frege133  44441  clsk1indlem3  44488  permaxinf2lem  45457  fnchoice  45478  limcresiooub  46088  limcresioolb  46089  fourierdlem48  46600  fourierdlem49  46601  fourierdlem102  46654  fourierdlem114  46666  sge0resplit  46852  elpglem2  50199