Theorem unex 7720

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

Syntax hints:   ∈ wcel 2109  Vcvv 3447   ∪ cun 3912

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 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

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 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-sn 4590  df-pr 4592  df-uni 4872

This theorem is referenced by:  tpex  7722  unexbOLD  7724  fvclex  7937  naddcllem  8640  ralxpmap  8869  unen  9017  undom  9029  enfixsn  9050  sbthlem10  9060  dif1en  9124  dif1enOLD  9126  findcard2  9128  unxpdomlem3  9199  isinf  9207  isinfOLD  9208  ac6sfi  9231  pwfilem  9267  cnfcomlem  9652  trcl  9681  tc2  9695  rankxpu  9829  rankxplim  9832  rankxplim3  9834  r0weon  9965  infxpenlem  9966  dfac4  10075  dfac2b  10084  kmlem2  10105  cfsmolem  10223  isfin1-3  10339  axdc2lem  10401  axdc3lem4  10406  axcclem  10410  ttukeylem3  10464  gchac  10634  wunex2  10691  wuncval2  10700  inar1  10728  nn0ex  12448  xrex  12946  seqexw  13982  hashbclem  14417  incexclem  15802  ramub1lem2  16998  prdsval  17418  imasval  17474  ipoval  18489  plusffval  18573  smndex1bas  18833  smndex1sgrp  18835  smndex1mnd  18837  smndex1id  18838  grpinvfval  18910  grpsubfval  18915  mulgfval  19001  staffval  20750  scaffval  20786  lpival  21234  cnfldex  21267  xrsex  21294  ipffval  21557  islindf4  21747  psrval  21824  neitr  23067  leordtval2  23099  comppfsc  23419  1stckgen  23441  dfac14  23505  ptcmpfi  23700  hausflim  23868  flimclslem  23871  alexsubALTlem2  23935  nmfval  24476  icccmplem2  24712  tcphex  25117  tchnmfval  25128  taylfval  26266  lrrecse  27849  addsval  27869  negsval  27931  negsid  27947  mulsval  28012  mulsproplem9  28027  precsexlem4  28112  precsexlem5  28113  onscutlt  28165  onaddscl  28174  legval  28511  axlowdimlem15  28883  axlowdim  28888  eengv  28906  uhgrunop  29002  upgrunop  29046  umgrunop  29048  padct  32643  cycpmconjslem2  33112  rlocbas  33218  rlocaddval  33219  rlocmulval  33220  idlsrgval  33474  ordtconnlem1  33914  sxbrsigalem2  34277  actfunsnf1o  34595  actfunsnrndisj  34596  reprsuc  34606  breprexplema  34621  bnj918  34756  fineqvac  35087  subfacp1lem3  35169  subfacp1lem5  35171  erdszelem8  35185  satfvsuclem1  35346  satf0suc  35363  fmlasuc0  35371  mrexval  35488  mrsubcv  35497  mrsubff  35499  mrsubccat  35505  elmrsubrn  35507  rdgssun  37366  exrecfnlem  37367  finixpnum  37599  poimirlem4  37618  poimirlem15  37629  poimirlem28  37642  rrnval  37821  lsatset  38983  ldualset  39118  pclfinN  39894  dvaset  40999  dvhset  41075  hlhilset  41928  evlselv  42575  elrfi  42682  istopclsd  42688  mzpcompact2lem  42739  eldioph2lem1  42748  eldioph2lem2  42749  eldioph4b  42799  diophren  42801  ttac  43025  pwslnmlem2  43082  dfacbasgrp  43097  mendval  43168  idomsubgmo  43182  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  permaxinf2lem  45002  fnchoice  45023  limcresiooub  45640  limcresioolb  45641  fourierdlem48  46152  fourierdlem49  46153  fourierdlem102  46206  fourierdlem114  46218  sge0resplit  46404  elpglem2  49701