Theorem unex 7699

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

Syntax hints:   ∈ wcel 2114  Vcvv 3442   ∪ cun 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920  df-sn 4583  df-pr 4585  df-uni 4866

This theorem is referenced by:  tpex  7701  unexbOLD  7703  fvclex  7913  naddcllem  8614  ralxpmap  8846  unen  8994  undom  9005  enfixsn  9026  sbthlem10  9036  dif1en  9098  findcard2  9101  unxpdomlem3  9170  isinf  9177  ac6sfi  9196  pwfilem  9230  cnfcomlem  9620  trcl  9649  tc2  9661  rankxpu  9800  rankxplim  9803  rankxplim3  9805  r0weon  9934  infxpenlem  9935  dfac4  10044  dfac2b  10053  kmlem2  10074  cfsmolem  10192  isfin1-3  10308  axdc2lem  10370  axdc3lem4  10375  axcclem  10379  ttukeylem3  10433  gchac  10604  wunex2  10661  wuncval2  10670  inar1  10698  nn0ex  12419  xrex  12912  seqexw  13952  hashbclem  14387  incexclem  15771  ramub1lem2  16967  prdsval  17387  imasval  17444  ipoval  18465  plusffval  18583  smndex1bas  18843  smndex1sgrp  18845  smndex1mnd  18847  smndex1id  18848  grpinvfval  18920  grpsubfval  18925  mulgfval  19011  staffval  20786  scaffval  20843  lpival  21291  cnfldex  21324  xrsex  21351  ipffval  21615  islindf4  21805  psrval  21883  neitr  23136  leordtval2  23168  comppfsc  23488  1stckgen  23510  dfac14  23574  ptcmpfi  23769  hausflim  23937  flimclslem  23940  alexsubALTlem2  24004  nmfval  24544  icccmplem2  24780  tcphex  25185  tchnmfval  25196  taylfval  26334  lrrecse  27950  addsval  27970  negsval  28033  negsid  28049  mulsval  28117  mulsproplem9  28132  precsexlem4  28218  precsexlem5  28219  oncutlt  28272  onaddscl  28285  legval  28668  axlowdimlem15  29041  axlowdim  29046  eengv  29064  uhgrunop  29160  upgrunop  29204  umgrunop  29206  padct  32807  cycpmconjslem2  33248  rlocbas  33360  rlocaddval  33361  rlocmulval  33362  idlsrgval  33595  ordtconnlem1  34101  sxbrsigalem2  34463  actfunsnf1o  34781  actfunsnrndisj  34782  reprsuc  34792  breprexplema  34807  bnj918  34942  fineqvac  35291  subfacp1lem3  35395  subfacp1lem5  35397  erdszelem8  35411  satfvsuclem1  35572  satf0suc  35589  fmlasuc0  35597  mrexval  35714  mrsubcv  35723  mrsubff  35725  mrsubccat  35731  elmrsubrn  35733  rdgssun  37627  exrecfnlem  37628  finixpnum  37850  poimirlem4  37869  poimirlem15  37880  poimirlem28  37893  rrnval  38072  lsatset  39360  ldualset  39495  pclfinN  40270  dvaset  41375  dvhset  41451  hlhilset  42304  evlselv  42939  elrfi  43045  istopclsd  43051  mzpcompact2lem  43102  eldioph2lem1  43111  eldioph2lem2  43112  eldioph4b  43162  diophren  43164  ttac  43387  pwslnmlem2  43444  dfacbasgrp  43459  mendval  43530  idomsubgmo  43544  superuncl  43918  ssuncl  43920  sssymdifcl  43922  rclexi  43965  trclexi  43970  rtrclexi  43971  dfrtrcl5  43979  dfrcl2  44024  comptiunov2i  44056  cotrclrcl  44092  frege83  44296  frege110  44323  frege133  44346  clsk1indlem3  44393  permaxinf2lem  45362  fnchoice  45383  limcresiooub  45994  limcresioolb  45995  fourierdlem48  46506  fourierdlem49  46507  fourierdlem102  46560  fourierdlem114  46572  sge0resplit  46758  elpglem2  50065