Theorem unex 7686

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

Syntax hints:   ∈ wcel 2113  Vcvv 3438   ∪ cun 3897

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 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7677

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-sn 4578  df-pr 4580  df-uni 4861

This theorem is referenced by:  tpex  7688  unexbOLD  7690  fvclex  7900  naddcllem  8600  ralxpmap  8829  unen  8977  undom  8988  enfixsn  9009  sbthlem10  9019  dif1en  9081  findcard2  9084  unxpdomlem3  9152  isinf  9159  ac6sfi  9178  pwfilem  9212  cnfcomlem  9599  trcl  9628  tc2  9640  rankxpu  9779  rankxplim  9782  rankxplim3  9784  r0weon  9913  infxpenlem  9914  dfac4  10023  dfac2b  10032  kmlem2  10053  cfsmolem  10171  isfin1-3  10287  axdc2lem  10349  axdc3lem4  10354  axcclem  10358  ttukeylem3  10412  gchac  10582  wunex2  10639  wuncval2  10648  inar1  10676  nn0ex  12397  xrex  12895  seqexw  13934  hashbclem  14369  incexclem  15753  ramub1lem2  16949  prdsval  17369  imasval  17425  ipoval  18446  plusffval  18564  smndex1bas  18824  smndex1sgrp  18826  smndex1mnd  18828  smndex1id  18829  grpinvfval  18901  grpsubfval  18906  mulgfval  18992  staffval  20766  scaffval  20823  lpival  21271  cnfldex  21304  xrsex  21331  ipffval  21595  islindf4  21785  psrval  21862  neitr  23105  leordtval2  23137  comppfsc  23457  1stckgen  23479  dfac14  23543  ptcmpfi  23738  hausflim  23906  flimclslem  23909  alexsubALTlem2  23973  nmfval  24513  icccmplem2  24749  tcphex  25154  tchnmfval  25165  taylfval  26303  lrrecse  27895  addsval  27915  negsval  27977  negsid  27993  mulsval  28058  mulsproplem9  28073  precsexlem4  28158  precsexlem5  28159  onscutlt  28211  onaddscl  28220  legval  28572  axlowdimlem15  28945  axlowdim  28950  eengv  28968  uhgrunop  29064  upgrunop  29108  umgrunop  29110  padct  32712  cycpmconjslem2  33135  rlocbas  33245  rlocaddval  33246  rlocmulval  33247  idlsrgval  33479  ordtconnlem1  33948  sxbrsigalem2  34310  actfunsnf1o  34628  actfunsnrndisj  34629  reprsuc  34639  breprexplema  34654  bnj918  34789  fineqvac  35150  subfacp1lem3  35237  subfacp1lem5  35239  erdszelem8  35253  satfvsuclem1  35414  satf0suc  35431  fmlasuc0  35439  mrexval  35556  mrsubcv  35565  mrsubff  35567  mrsubccat  35573  elmrsubrn  35575  rdgssun  37433  exrecfnlem  37434  finixpnum  37655  poimirlem4  37674  poimirlem15  37685  poimirlem28  37698  rrnval  37877  lsatset  39099  ldualset  39234  pclfinN  40009  dvaset  41114  dvhset  41190  hlhilset  42043  evlselv  42695  elrfi  42801  istopclsd  42807  mzpcompact2lem  42858  eldioph2lem1  42867  eldioph2lem2  42868  eldioph4b  42918  diophren  42920  ttac  43143  pwslnmlem2  43200  dfacbasgrp  43215  mendval  43286  idomsubgmo  43300  superuncl  43675  ssuncl  43677  sssymdifcl  43679  rclexi  43722  trclexi  43727  rtrclexi  43728  dfrtrcl5  43736  dfrcl2  43781  comptiunov2i  43813  cotrclrcl  43849  frege83  44053  frege110  44080  frege133  44103  clsk1indlem3  44150  permaxinf2lem  45119  fnchoice  45140  limcresiooub  45754  limcresioolb  45755  fourierdlem48  46266  fourierdlem49  46267  fourierdlem102  46320  fourierdlem114  46332  sge0resplit  46518  elpglem2  49827