Theorem unex 7723

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

Syntax hints:   ∈ wcel 2141  Vcvv 3453   ∪ cun 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-pr 5389  ax-un 7714

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3909  df-ss 3921  df-sn 4582  df-pr 4584  df-uni 4865

This theorem is referenced by:  tpex  7725  unexbOLD  7727  fvclex  7936  naddcllem  8641  ralxpmap  8874  unen  9022  undom  9033  enfixsn  9054  sbthlem10  9064  dif1en  9126  findcard2  9129  unxpdomlem3  9198  isinf  9205  ac6sfi  9224  pwfilem  9258  cnfcomlem  9651  trcl  9680  tc2  9692  rankxpu  9831  rankxplim  9834  rankxplim3  9836  r0weon  9965  infxpenlem  9966  dfac4  10075  dfac2b  10084  kmlem2  10105  cfsmolem  10224  isfin1-3  10340  axdc2lem  10402  axdc3lem4  10407  axcclem  10411  ttukeylem3  10465  gchac  10636  wunex2  10693  wuncval2  10702  inar1  10730  nn0ex  12484  xrex  12985  seqexw  14027  hashbclem  14462  incexclem  15849  ramub1lem2  17046  prdsval  17467  imasval  17524  ipoval  18545  plusffval  18663  smndex1bas  18926  smndex1sgrp  18928  smndex1mnd  18930  smndex1id  18931  grpinvfval  19003  grpsubfval  19008  mulgfval  19094  staffval  20870  scaffval  20927  lpival  21374  cnfldex  21407  xrsex  21421  ipffval  21680  islindf4  21870  psrval  21947  neitr  23220  leordtval2  23252  comppfsc  23572  1stckgen  23594  dfac14  23658  ptcmpfi  23853  hausflim  24021  flimclslem  24024  alexsubALTlem2  24088  nmfval  24628  icccmplem2  24864  tcphex  25259  tchnmfval  25270  taylfval  26399  lrrecse  28012  addsval  28032  negsval  28095  negsid  28111  mulsval  28179  mulsproplem9  28194  precsexlem4  28280  precsexlem5  28281  oncutlt  28334  onaddscl  28347  legval  28730  axlowdimlem15  29103  axlowdim  29108  eengv  29126  uhgrunop  29222  upgrunop  29266  umgrunop  29268  padct  32870  cycpmconjslem2  33296  rlocbas  33410  rlocaddval  33411  rlocmulval  33412  idlsrgval  33660  ordtconnlem1  34182  sxbrsigalem2  34544  actfunsnf1o  34862  actfunsnrndisj  34863  reprsuc  34873  breprexplema  34888  bnj918  35026  fineqvac  35376  subfacp1lem3  35496  subfacp1lem5  35498  erdszelem8  35512  satfvsuclem1  35673  satf0suc  35690  fmlasuc0  35698  mrexval  35815  mrsubcv  35824  mrsubff  35826  mrsubccat  35832  elmrsubrn  35834  dfttc4lem2  36853  rdgssun  37836  exrecfnlem  37837  finixpnum  38068  poimirlem4  38087  poimirlem15  38098  poimirlem28  38111  rrnval  38290  lsatset  39578  ldualset  39713  pclfinN  40488  dvaset  41593  dvhset  41669  hlhilset  42522  evlselv  43135  elrfi  43239  istopclsd  43245  mzpcompact2lem  43296  eldioph2lem1  43305  eldioph2lem2  43306  eldioph4b  43352  diophren  43354  ttac  43577  pwslnmlem2  43634  dfacbasgrp  43649  mendval  43720  idomsubgmo  43734  superuncl  44108  ssuncl  44110  sssymdifcl  44112  rclexi  44155  trclexi  44160  rtrclexi  44161  dfrtrcl5  44169  dfrcl2  44214  comptiunov2i  44246  cotrclrcl  44282  frege83  44486  frege110  44513  frege133  44536  clsk1indlem3  44583  permaxinf2lem  45552  fnchoice  45573  limcresiooub  46180  limcresioolb  46181  fourierdlem48  46692  fourierdlem49  46693  fourierdlem102  46746  fourierdlem114  46758  sge0resplit  46944  elpglem2  50297