Theorem unex 7764

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

Syntax hints:   ∈ wcel 2108  Vcvv 3480   ∪ cun 3949

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-sn 4627  df-pr 4629  df-uni 4908

This theorem is referenced by:  tpex  7766  unexbOLD  7768  fvclex  7983  naddcllem  8714  ralxpmap  8936  unen  9086  undom  9099  enfixsn  9121  sbthlem10  9132  dif1en  9200  dif1enOLD  9202  findcard2  9204  unxpdomlem3  9288  isinf  9296  isinfOLD  9297  ac6sfi  9320  pwfilem  9356  cnfcomlem  9739  trcl  9768  tc2  9782  rankxpu  9916  rankxplim  9919  rankxplim3  9921  r0weon  10052  infxpenlem  10053  dfac4  10162  dfac2b  10171  kmlem2  10192  cfsmolem  10310  isfin1-3  10426  axdc2lem  10488  axdc3lem4  10493  axcclem  10497  ttukeylem3  10551  gchac  10721  wunex2  10778  wuncval2  10787  inar1  10815  nn0ex  12532  xrex  13029  seqexw  14058  hashbclem  14491  incexclem  15872  ramub1lem2  17065  prdsval  17500  imasval  17556  ipoval  18575  plusffval  18659  smndex1bas  18919  smndex1sgrp  18921  smndex1mnd  18923  smndex1id  18924  grpinvfval  18996  grpsubfval  19001  mulgfval  19087  staffval  20842  scaffval  20878  lpival  21334  cnfldex  21367  xrsex  21395  ipffval  21666  islindf4  21858  psrval  21935  neitr  23188  leordtval2  23220  comppfsc  23540  1stckgen  23562  dfac14  23626  ptcmpfi  23821  hausflim  23989  flimclslem  23992  alexsubALTlem2  24056  nmfval  24601  icccmplem2  24845  tcphex  25251  tchnmfval  25262  taylfval  26400  lrrecse  27975  addsval  27995  negsval  28057  negsid  28073  mulsval  28135  mulsproplem9  28150  precsexlem4  28234  precsexlem5  28235  onaddscl  28286  legval  28592  axlowdimlem15  28971  axlowdim  28976  eengv  28994  uhgrunop  29092  upgrunop  29136  umgrunop  29138  padct  32731  cycpmconjslem2  33175  rlocbas  33271  rlocaddval  33272  rlocmulval  33273  idlsrgval  33531  ordtconnlem1  33923  sxbrsigalem2  34288  actfunsnf1o  34619  actfunsnrndisj  34620  reprsuc  34630  breprexplema  34645  bnj918  34780  fineqvac  35111  subfacp1lem3  35187  subfacp1lem5  35189  erdszelem8  35203  satfvsuclem1  35364  satf0suc  35381  fmlasuc0  35389  mrexval  35506  mrsubcv  35515  mrsubff  35517  mrsubccat  35523  elmrsubrn  35525  rdgssun  37379  exrecfnlem  37380  finixpnum  37612  poimirlem4  37631  poimirlem15  37642  poimirlem28  37655  rrnval  37834  lsatset  38991  ldualset  39126  pclfinN  39902  dvaset  41007  dvhset  41083  hlhilset  41936  evlselv  42597  elrfi  42705  istopclsd  42711  mzpcompact2lem  42762  eldioph2lem1  42771  eldioph2lem2  42772  eldioph4b  42822  diophren  42824  ttac  43048  pwslnmlem2  43105  dfacbasgrp  43120  mendval  43191  idomsubgmo  43205  superuncl  43581  ssuncl  43583  sssymdifcl  43585  rclexi  43628  trclexi  43633  rtrclexi  43634  dfrtrcl5  43642  dfrcl2  43687  comptiunov2i  43719  cotrclrcl  43755  frege83  43959  frege110  43986  frege133  44009  clsk1indlem3  44056  fnchoice  45034  limcresiooub  45657  limcresioolb  45658  fourierdlem48  46169  fourierdlem49  46170  fourierdlem102  46223  fourierdlem114  46235  sge0resplit  46421  elpglem2  49231