Theorem unex 7698

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

Syntax hints:   ∈ wcel 2114  Vcvv 3429   ∪ cun 3887

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 2708  ax-sep 5231  ax-pr 5375  ax-un 7689

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-sn 4568  df-pr 4570  df-uni 4851

This theorem is referenced by:  tpex  7700  unexbOLD  7702  fvclex  7912  naddcllem  8612  ralxpmap  8844  unen  8992  undom  9003  enfixsn  9024  sbthlem10  9034  dif1en  9096  findcard2  9099  unxpdomlem3  9168  isinf  9175  ac6sfi  9194  pwfilem  9228  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  12443  xrex  12937  seqexw  13979  hashbclem  14414  incexclem  15801  ramub1lem2  16998  prdsval  17418  imasval  17475  ipoval  18496  plusffval  18614  smndex1bas  18877  smndex1sgrp  18879  smndex1mnd  18881  smndex1id  18882  grpinvfval  18954  grpsubfval  18959  mulgfval  19045  staffval  20818  scaffval  20875  lpival  21322  cnfldex  21355  xrsex  21369  ipffval  21628  islindf4  21818  psrval  21895  neitr  23145  leordtval2  23177  comppfsc  23497  1stckgen  23519  dfac14  23583  ptcmpfi  23778  hausflim  23946  flimclslem  23949  alexsubALTlem2  24013  nmfval  24553  icccmplem2  24789  tcphex  25184  tchnmfval  25195  taylfval  26324  lrrecse  27934  addsval  27954  negsval  28017  negsid  28033  mulsval  28101  mulsproplem9  28116  precsexlem4  28202  precsexlem5  28203  oncutlt  28256  onaddscl  28269  legval  28652  axlowdimlem15  29025  axlowdim  29030  eengv  29048  uhgrunop  29144  upgrunop  29188  umgrunop  29190  padct  32791  cycpmconjslem2  33216  rlocbas  33328  rlocaddval  33329  rlocmulval  33330  idlsrgval  33563  ordtconnlem1  34068  sxbrsigalem2  34430  actfunsnf1o  34748  actfunsnrndisj  34749  reprsuc  34759  breprexplema  34774  bnj918  34909  fineqvac  35260  subfacp1lem3  35364  subfacp1lem5  35366  erdszelem8  35380  satfvsuclem1  35541  satf0suc  35558  fmlasuc0  35566  mrexval  35683  mrsubcv  35692  mrsubff  35694  mrsubccat  35700  elmrsubrn  35702  dfttc4lem2  36711  rdgssun  37694  exrecfnlem  37695  finixpnum  37926  poimirlem4  37945  poimirlem15  37956  poimirlem28  37969  rrnval  38148  lsatset  39436  ldualset  39571  pclfinN  40346  dvaset  41451  dvhset  41527  hlhilset  42380  evlselv  43020  elrfi  43126  istopclsd  43132  mzpcompact2lem  43183  eldioph2lem1  43192  eldioph2lem2  43193  eldioph4b  43239  diophren  43241  ttac  43464  pwslnmlem2  43521  dfacbasgrp  43536  mendval  43607  idomsubgmo  43621  superuncl  43995  ssuncl  43997  sssymdifcl  43999  rclexi  44042  trclexi  44047  rtrclexi  44048  dfrtrcl5  44056  dfrcl2  44101  comptiunov2i  44133  cotrclrcl  44169  frege83  44373  frege110  44400  frege133  44423  clsk1indlem3  44470  permaxinf2lem  45439  fnchoice  45460  limcresiooub  46070  limcresioolb  46071  fourierdlem48  46582  fourierdlem49  46583  fourierdlem102  46636  fourierdlem114  46648  sge0resplit  46834  elpglem2  50187