Theorem unex 7684

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

Syntax hints:   ∈ wcel 2109  Vcvv 3438   ∪ cun 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-sn 4580  df-pr 4582  df-uni 4862

This theorem is referenced by:  tpex  7686  unexbOLD  7688  fvclex  7901  naddcllem  8601  ralxpmap  8830  unen  8978  undom  8989  enfixsn  9010  sbthlem10  9020  dif1en  9084  dif1enOLD  9086  findcard2  9088  unxpdomlem3  9157  isinf  9165  isinfOLD  9166  ac6sfi  9189  pwfilem  9225  cnfcomlem  9614  trcl  9643  tc2  9657  rankxpu  9791  rankxplim  9794  rankxplim3  9796  r0weon  9925  infxpenlem  9926  dfac4  10035  dfac2b  10044  kmlem2  10065  cfsmolem  10183  isfin1-3  10299  axdc2lem  10361  axdc3lem4  10366  axcclem  10370  ttukeylem3  10424  gchac  10594  wunex2  10651  wuncval2  10660  inar1  10688  nn0ex  12408  xrex  12906  seqexw  13942  hashbclem  14377  incexclem  15761  ramub1lem2  16957  prdsval  17377  imasval  17433  ipoval  18454  plusffval  18538  smndex1bas  18798  smndex1sgrp  18800  smndex1mnd  18802  smndex1id  18803  grpinvfval  18875  grpsubfval  18880  mulgfval  18966  staffval  20744  scaffval  20801  lpival  21249  cnfldex  21282  xrsex  21309  ipffval  21573  islindf4  21763  psrval  21840  neitr  23083  leordtval2  23115  comppfsc  23435  1stckgen  23457  dfac14  23521  ptcmpfi  23716  hausflim  23884  flimclslem  23887  alexsubALTlem2  23951  nmfval  24492  icccmplem2  24728  tcphex  25133  tchnmfval  25144  taylfval  26282  lrrecse  27872  addsval  27892  negsval  27954  negsid  27970  mulsval  28035  mulsproplem9  28050  precsexlem4  28135  precsexlem5  28136  onscutlt  28188  onaddscl  28197  legval  28547  axlowdimlem15  28919  axlowdim  28924  eengv  28942  uhgrunop  29038  upgrunop  29082  umgrunop  29084  padct  32676  cycpmconjslem2  33110  rlocbas  33217  rlocaddval  33218  rlocmulval  33219  idlsrgval  33450  ordtconnlem1  33890  sxbrsigalem2  34253  actfunsnf1o  34571  actfunsnrndisj  34572  reprsuc  34582  breprexplema  34597  bnj918  34732  fineqvac  35071  subfacp1lem3  35154  subfacp1lem5  35156  erdszelem8  35170  satfvsuclem1  35331  satf0suc  35348  fmlasuc0  35356  mrexval  35473  mrsubcv  35482  mrsubff  35484  mrsubccat  35490  elmrsubrn  35492  rdgssun  37351  exrecfnlem  37352  finixpnum  37584  poimirlem4  37603  poimirlem15  37614  poimirlem28  37627  rrnval  37806  lsatset  38968  ldualset  39103  pclfinN  39879  dvaset  40984  dvhset  41060  hlhilset  41913  evlselv  42560  elrfi  42667  istopclsd  42673  mzpcompact2lem  42724  eldioph2lem1  42733  eldioph2lem2  42734  eldioph4b  42784  diophren  42786  ttac  43009  pwslnmlem2  43066  dfacbasgrp  43081  mendval  43152  idomsubgmo  43166  superuncl  43541  ssuncl  43543  sssymdifcl  43545  rclexi  43588  trclexi  43593  rtrclexi  43594  dfrtrcl5  43602  dfrcl2  43647  comptiunov2i  43679  cotrclrcl  43715  frege83  43919  frege110  43946  frege133  43969  clsk1indlem3  44016  permaxinf2lem  44986  fnchoice  45007  limcresiooub  45624  limcresioolb  45625  fourierdlem48  46136  fourierdlem49  46137  fourierdlem102  46190  fourierdlem114  46202  sge0resplit  46388  elpglem2  49698