Theorem unex 7762

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

Syntax hints:   ∈ wcel 2105  Vcvv 3477   ∪ cun 3960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-sn 4631  df-pr 4633  df-uni 4912

This theorem is referenced by:  tpex  7764  unexbOLD  7766  fvclex  7981  naddcllem  8712  ralxpmap  8934  unen  9084  undom  9097  enfixsn  9119  sbthlem10  9130  dif1en  9198  dif1enOLD  9200  findcard2  9202  unxpdomlem3  9285  isinf  9293  isinfOLD  9294  ac6sfi  9317  pwfilem  9353  cnfcomlem  9736  trcl  9765  tc2  9779  rankxpu  9913  rankxplim  9916  rankxplim3  9918  r0weon  10049  infxpenlem  10050  dfac4  10159  dfac2b  10168  kmlem2  10189  cfsmolem  10307  isfin1-3  10423  axdc2lem  10485  axdc3lem4  10490  axcclem  10494  ttukeylem3  10548  gchac  10718  wunex2  10775  wuncval2  10784  inar1  10812  nn0ex  12529  xrex  13026  seqexw  14054  hashbclem  14487  incexclem  15868  ramub1lem2  17060  prdsval  17501  imasval  17557  ipoval  18587  plusffval  18671  smndex1bas  18931  smndex1sgrp  18933  smndex1mnd  18935  smndex1id  18936  grpinvfval  19008  grpsubfval  19013  mulgfval  19099  staffval  20858  scaffval  20894  lpival  21351  cnfldex  21384  xrsex  21412  ipffval  21683  islindf4  21875  psrval  21952  neitr  23203  leordtval2  23235  comppfsc  23555  1stckgen  23577  dfac14  23641  ptcmpfi  23836  hausflim  24004  flimclslem  24007  alexsubALTlem2  24071  nmfval  24616  icccmplem2  24858  tcphex  25264  tchnmfval  25275  taylfval  26414  lrrecse  27989  addsval  28009  negsval  28071  negsid  28087  mulsval  28149  mulsproplem9  28164  precsexlem4  28248  precsexlem5  28249  onaddscl  28300  legval  28606  axlowdimlem15  28985  axlowdim  28990  eengv  29008  uhgrunop  29106  upgrunop  29150  umgrunop  29152  padct  32736  cycpmconjslem2  33157  rlocbas  33253  rlocaddval  33254  rlocmulval  33255  idlsrgval  33510  ordtconnlem1  33884  sxbrsigalem2  34267  actfunsnf1o  34597  actfunsnrndisj  34598  reprsuc  34608  breprexplema  34623  bnj918  34758  fineqvac  35089  subfacp1lem3  35166  subfacp1lem5  35168  erdszelem8  35182  satfvsuclem1  35343  satf0suc  35360  fmlasuc0  35368  mrexval  35485  mrsubcv  35494  mrsubff  35496  mrsubccat  35502  elmrsubrn  35504  rdgssun  37360  exrecfnlem  37361  finixpnum  37591  poimirlem4  37610  poimirlem15  37621  poimirlem28  37634  rrnval  37813  lsatset  38971  ldualset  39106  pclfinN  39882  dvaset  40987  dvhset  41063  hlhilset  41916  evlselv  42573  elrfi  42681  istopclsd  42687  mzpcompact2lem  42738  eldioph2lem1  42747  eldioph2lem2  42748  eldioph4b  42798  diophren  42800  ttac  43024  pwslnmlem2  43081  dfacbasgrp  43096  mendval  43167  idomsubgmo  43181  superuncl  43557  ssuncl  43559  sssymdifcl  43561  rclexi  43604  trclexi  43609  rtrclexi  43610  dfrtrcl5  43618  dfrcl2  43663  comptiunov2i  43695  cotrclrcl  43731  frege83  43935  frege110  43962  frege133  43985  clsk1indlem3  44032  fnchoice  44966  limcresiooub  45597  limcresioolb  45598  fourierdlem48  46109  fourierdlem49  46110  fourierdlem102  46163  fourierdlem114  46175  sge0resplit  46361  elpglem2  48942