Theorem unex 7694

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

Syntax hints:   ∈ wcel 2119  Vcvv 3432   ∪ cun 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-ss 3907  df-sn 4563  df-pr 4565  df-uni 4846

This theorem is referenced by:  tpex  7696  unexbOLD  7698  fvclex  7908  naddcllem  8609  ralxpmap  8841  unen  8989  undom  9000  enfixsn  9021  sbthlem10  9031  dif1en  9093  findcard2  9096  unxpdomlem3  9165  isinf  9172  ac6sfi  9191  pwfilem  9225  cnfcomlem  9618  trcl  9647  tc2  9659  rankxpu  9798  rankxplim  9801  rankxplim3  9803  r0weon  9932  infxpenlem  9933  dfac4  10042  dfac2b  10051  kmlem2  10072  cfsmolem  10190  isfin1-3  10306  axdc2lem  10368  axdc3lem4  10373  axcclem  10377  ttukeylem3  10431  gchac  10602  wunex2  10659  wuncval2  10668  inar1  10696  nn0ex  12441  xrex  12935  seqexw  13977  hashbclem  14412  incexclem  15799  ramub1lem2  16996  prdsval  17416  imasval  17473  ipoval  18494  plusffval  18612  smndex1bas  18875  smndex1sgrp  18877  smndex1mnd  18879  smndex1id  18880  grpinvfval  18952  grpsubfval  18957  mulgfval  19043  staffval  20820  scaffval  20877  lpival  21324  cnfldex  21357  xrsex  21371  ipffval  21630  islindf4  21820  psrval  21897  neitr  23170  leordtval2  23202  comppfsc  23522  1stckgen  23544  dfac14  23608  ptcmpfi  23803  hausflim  23971  flimclslem  23974  alexsubALTlem2  24038  nmfval  24578  icccmplem2  24814  tcphex  25209  tchnmfval  25220  taylfval  26349  lrrecse  27959  addsval  27979  negsval  28042  negsid  28058  mulsval  28126  mulsproplem9  28141  precsexlem4  28227  precsexlem5  28228  oncutlt  28281  onaddscl  28294  legval  28677  axlowdimlem15  29050  axlowdim  29055  eengv  29073  uhgrunop  29169  upgrunop  29213  umgrunop  29215  padct  32817  cycpmconjslem2  33243  rlocbas  33355  rlocaddval  33356  rlocmulval  33357  idlsrgval  33593  ordtconnlem1  34115  sxbrsigalem2  34477  actfunsnf1o  34795  actfunsnrndisj  34796  reprsuc  34806  breprexplema  34821  bnj918  34956  fineqvac  35304  subfacp1lem3  35417  subfacp1lem5  35419  erdszelem8  35433  satfvsuclem1  35594  satf0suc  35611  fmlasuc0  35619  mrexval  35736  mrsubcv  35745  mrsubff  35747  mrsubccat  35753  elmrsubrn  35755  dfttc4lem2  36764  rdgssun  37747  exrecfnlem  37748  finixpnum  37979  poimirlem4  37998  poimirlem15  38009  poimirlem28  38022  rrnval  38201  lsatset  39489  ldualset  39624  pclfinN  40399  dvaset  41504  dvhset  41580  hlhilset  42433  evlselv  43046  elrfi  43150  istopclsd  43156  mzpcompact2lem  43207  eldioph2lem1  43216  eldioph2lem2  43217  eldioph4b  43263  diophren  43265  ttac  43488  pwslnmlem2  43545  dfacbasgrp  43560  mendval  43631  idomsubgmo  43645  superuncl  44019  ssuncl  44021  sssymdifcl  44023  rclexi  44066  trclexi  44071  rtrclexi  44072  dfrtrcl5  44080  dfrcl2  44125  comptiunov2i  44157  cotrclrcl  44193  frege83  44397  frege110  44424  frege133  44447  clsk1indlem3  44494  permaxinf2lem  45463  fnchoice  45484  limcresiooub  46092  limcresioolb  46093  fourierdlem48  46604  fourierdlem49  46605  fourierdlem102  46658  fourierdlem114  46670  sge0resplit  46856  elpglem2  50209