Theorem unex 7731

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

Syntax hints:   ∈ wcel 2145  Vcvv 3457   ∪ cun 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251  ax-pr 5395  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-ss 3924  df-sn 4586  df-pr 4588  df-uni 4869

This theorem is referenced by:  tpex  7733  unexbOLD  7735  fvclex  7944  naddcllem  8650  ralxpmap  8882  unen  9030  undom  9041  enfixsn  9062  sbthlem10  9072  dif1en  9134  findcard2  9137  unxpdomlem3  9206  isinf  9213  ac6sfi  9232  pwfilem  9265  cnfcomlem  9656  trcl  9685  tc2  9697  rankxpu  9836  rankxplim  9839  rankxplim3  9841  r0weon  9984  infxpenlem  9985  dfac4  10094  dfac2b  10102  kmlem2  10123  cfsmolem  10242  isfin1-3  10358  axdc2lem  10420  axdc3lem4  10425  axcclem  10429  ttukeylem3  10483  gchac  10654  wunex2  10711  wuncval2  10720  inar1  10748  nn0ex  12501  xrex  13002  seqexw  14044  hashbclem  14479  incexclem  15880  ramub1lem2  17077  prdsval  17498  imasval  17555  ipoval  18576  plusffval  18694  smndex1bas  18958  smndex1sgrp  18960  smndex1mnd  18962  smndex1id  18963  grpinvfval  19035  grpsubfval  19040  mulgfval  19126  staffval  20913  scaffval  20970  lpival  21452  cnfldex  21485  xrsex  21499  ipffval  21758  islindf4  21948  psrval  22025  neitr  23298  leordtval2  23330  comppfsc  23650  1stckgen  23672  dfac14  23736  ptcmpfi  23931  hausflim  24099  flimclslem  24102  alexsubALTlem2  24166  nmfval  24706  icccmplem2  24942  tcphex  25337  tchnmfval  25348  taylfval  26480  lrrecse  28093  addsval  28113  negsval  28176  negsid  28192  mulsval  28260  mulsproplem9  28275  precsexlem4  28361  precsexlem5  28362  oncutlt  28415  onaddscl  28428  legval  28811  axlowdimlem15  29215  axlowdim  29220  eengv  29238  uhgrunop  29334  upgrunop  29378  umgrunop  29380  padct  32975  cycpmconjslem2  33388  rlocbas  33501  rlocaddval  33502  rlocmulval  33503  idlsrgval  33710  ordtconnlem1  34231  sxbrsigalem2  34593  actfunsnf1o  34908  actfunsnrndisj  34909  reprsuc  34919  breprexplema  34934  bnj918  35072  fineqvac  35424  subfacp1lem3  35545  subfacp1lem5  35547  erdszelem8  35561  satfvsuclem1  35722  satf0suc  35739  fmlasuc0  35747  mrexval  35864  mrsubcv  35873  mrsubff  35875  mrsubccat  35881  elmrsubrn  35883  dfttc4lem2  36902  rdgssun  37884  exrecfnlem  37885  finixpnum  38116  poimirlem4  38135  poimirlem15  38146  poimirlem28  38159  rrnval  38338  lsatset  39626  ldualset  39761  pclfinN  40536  dvaset  41641  dvhset  41717  hlhilset  42570  evlselv  43183  elrfi  43287  istopclsd  43293  mzpcompact2lem  43344  eldioph2lem1  43353  eldioph2lem2  43354  eldioph4b  43400  diophren  43402  ttac  43625  pwslnmlem2  43682  dfacbasgrp  43697  mendval  43768  idomsubgmo  43782  superuncl  44156  ssuncl  44158  sssymdifcl  44160  rclexi  44203  trclexi  44208  rtrclexi  44209  dfrtrcl5  44217  dfrcl2  44262  comptiunov2i  44294  cotrclrcl  44330  frege83  44534  frege110  44561  frege133  44584  clsk1indlem3  44631  permaxinf2lem  45586  fnchoice  45607  limcresiooub  46214  limcresioolb  46215  fourierdlem48  46726  fourierdlem49  46727  fourierdlem102  46780  fourierdlem114  46792  sge0resplit  46978  elpglem2  50341