Theorem unex 7788

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454   ∪ cun 4152

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-pr 5396  ax-un 7778

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-sn 4589  df-pr 4591  df-uni 4871

This theorem is used by:  tpex  7789  fvclex  7998  naddcllem  8716  ralxpmap  8955  unen  9104  undom  9115  enfixsn  9136  sbthlem10  9146  dif1en  9208  findcard2  9211  unxpdomlem3  9280  isinf  9287  ac6sfi  9306  pwfilem  9340  cnfcomlem  9730  trcl  9759  tc2  9771  rankxpu  9923  rankxplim  9926  rankxplim3  9928  r0weon  10121  infxpenlem  10122  dfac4  10231  dfac2b  10239  kmlem2  10260  cfsmolem  10378  isfin1-3  10494  axdc2lem  10556  axdc3lem4  10561  axcclem  10565  ttukeylem3  10619  gchac  10796  wunex2  10853  wuncval2  10862  inar1  10890  nn0ex  12642  xrex  13145  seqexw  14190  hashbclem  14627  incexclem  16037  ramub1lem2  17237  prdsval  17658  imasval  17715  ipoval  18736  plusffval  18854  smndex1bas  19137  smndex1sgrp  19139  smndex1mnd  19141  smndex1id  19142  grpinvfval  19221  grpsubfval  19226  mulgfval  19311  staffval  21131  scaffval  21188  lpival  21681  cnfldex  21714  xrsex  21728  ipffval  21987  islindf4  22177  psrval  22256  neitr  23531  leordtval2  23563  comppfsc  23884  1stckgen  23906  dfac14  23970  ptcmpfi  24165  hausflim  24333  flimclslem  24336  alexsubALTlem2  24400  nmfval  24940  icccmplem2  25176  tcphex  25571  tchnmfval  25582  taylfval  26719  lrrecse  28361  addsval  28381  negsval  28444  negsid  28460  mulsval  28528  mulsproplem9  28543  precsexlem4  28629  precsexlem5  28630  oncutlt  28683  onaddscl  28696  legval  29080  axlowdimlem15  29567  axlowdim  29572  eengv  29590  uhgrunop  29686  upgrunop  29730  umgrunop  29732  padct  33384  cycpmconjslem2  33792  rlocbas  33905  rlocaddval  33906  rlocmulval  33907  idlsrgval  34119  ordtconnlem1  34639  sxbrsigalem2  35001  actfunsnf1o  35316  actfunsnrndisj  35317  reprsuc  35327  breprexplema  35342  bnj918  35480  fineqvac  35897  subfacp1lem3  36127  subfacp1lem5  36129  erdszelem8  36143  satfvsuclem1  36304  satf0suc  36321  fmlasuc0  36329  mrexval  36446  mrsubcv  36455  mrsubff  36457  mrsubccat  36463  elmrsubrn  36465  dfttc4lem2  37508  rdgssun  38506  exrecfnlem  38507  finixpnum  38733  poimirlem4  38747  poimirlem15  38758  poimirlem28  38771  dfproplem  38846  rrnval  38964  lsatset  40250  ldualset  40385  pclfinN  41160  dvaset  42265  dvhset  42341  hlhilset  43194  evlselv  43821  elrfi  43909  istopclsd  43915  mzpcompact2lem  43966  eldioph2lem1  43975  eldioph2lem2  43976  eldioph4b  44022  diophren  44024  ttac  44247  pwslnmlem2  44299  dfacbasgrp  44313  mendval  44384  idomsubgmo  44398  superuncl  44772  ssuncl  44774  sssymdifcl  44776  rclexi  44818  trclexi  44823  rtrclexi  44824  dfrtrcl5  44832  dfrcl2  44877  comptiunov2i  44909  cotrclrcl  44945  frege83  45149  frege110  45176  frege133  45199  clsk1indlem3  45246  permaxinf2lem  46208  fnchoice  46262  limcresiooub  46867  limcresioolb  46868  fourierdlem48  47379  fourierdlem49  47380  fourierdlem102  47433  fourierdlem114  47445  sge0resplit  47631  parcatid2  50978  parcatid  50979  parmapfunc2  50989  elpglem2  51095