Theorem unex 7683

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

Syntax hints:   ∈ wcel 2113  Vcvv 3437   ∪ cun 3896

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 5236  ax-nul 5246  ax-pr 5372  ax-un 7674

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 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-sn 4576  df-pr 4578  df-uni 4859

This theorem is referenced by:  tpex  7685  unexbOLD  7687  fvclex  7897  naddcllem  8597  ralxpmap  8826  unen  8974  undom  8985  enfixsn  9006  sbthlem10  9016  dif1en  9078  findcard2  9081  unxpdomlem3  9149  isinf  9156  ac6sfi  9175  pwfilem  9209  cnfcomlem  9596  trcl  9625  tc2  9637  rankxpu  9776  rankxplim  9779  rankxplim3  9781  r0weon  9910  infxpenlem  9911  dfac4  10020  dfac2b  10029  kmlem2  10050  cfsmolem  10168  isfin1-3  10284  axdc2lem  10346  axdc3lem4  10351  axcclem  10355  ttukeylem3  10409  gchac  10579  wunex2  10636  wuncval2  10645  inar1  10673  nn0ex  12394  xrex  12887  seqexw  13926  hashbclem  14361  incexclem  15745  ramub1lem2  16941  prdsval  17361  imasval  17417  ipoval  18438  plusffval  18556  smndex1bas  18816  smndex1sgrp  18818  smndex1mnd  18820  smndex1id  18821  grpinvfval  18893  grpsubfval  18898  mulgfval  18984  staffval  20758  scaffval  20815  lpival  21263  cnfldex  21296  xrsex  21323  ipffval  21587  islindf4  21777  psrval  21854  neitr  23096  leordtval2  23128  comppfsc  23448  1stckgen  23470  dfac14  23534  ptcmpfi  23729  hausflim  23897  flimclslem  23900  alexsubALTlem2  23964  nmfval  24504  icccmplem2  24740  tcphex  25145  tchnmfval  25156  taylfval  26294  lrrecse  27886  addsval  27906  negsval  27968  negsid  27984  mulsval  28049  mulsproplem9  28064  precsexlem4  28149  precsexlem5  28150  onscutlt  28202  onaddscl  28211  legval  28563  axlowdimlem15  28936  axlowdim  28941  eengv  28959  uhgrunop  29055  upgrunop  29099  umgrunop  29101  padct  32705  cycpmconjslem2  33131  rlocbas  33241  rlocaddval  33242  rlocmulval  33243  idlsrgval  33475  ordtconnlem1  33958  sxbrsigalem2  34320  actfunsnf1o  34638  actfunsnrndisj  34639  reprsuc  34649  breprexplema  34664  bnj918  34799  fineqvac  35160  subfacp1lem3  35247  subfacp1lem5  35249  erdszelem8  35263  satfvsuclem1  35424  satf0suc  35441  fmlasuc0  35449  mrexval  35566  mrsubcv  35575  mrsubff  35577  mrsubccat  35583  elmrsubrn  35585  rdgssun  37443  exrecfnlem  37444  finixpnum  37665  poimirlem4  37684  poimirlem15  37695  poimirlem28  37708  rrnval  37887  lsatset  39109  ldualset  39244  pclfinN  40019  dvaset  41124  dvhset  41200  hlhilset  42053  evlselv  42705  elrfi  42811  istopclsd  42817  mzpcompact2lem  42868  eldioph2lem1  42877  eldioph2lem2  42878  eldioph4b  42928  diophren  42930  ttac  43153  pwslnmlem2  43210  dfacbasgrp  43225  mendval  43296  idomsubgmo  43310  superuncl  43685  ssuncl  43687  sssymdifcl  43689  rclexi  43732  trclexi  43737  rtrclexi  43738  dfrtrcl5  43746  dfrcl2  43791  comptiunov2i  43823  cotrclrcl  43859  frege83  44063  frege110  44090  frege133  44113  clsk1indlem3  44160  permaxinf2lem  45129  fnchoice  45150  limcresiooub  45764  limcresioolb  45765  fourierdlem48  46276  fourierdlem49  46277  fourierdlem102  46330  fourierdlem114  46342  sge0resplit  46528  elpglem2  49837