Theorem unex 7744

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

Syntax hints:   ∈ wcel 2143  Vcvv 3455   ∪ cun 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-ss 3923  df-sn 4591  df-pr 4593  df-uni 4874

This theorem is referenced by:  tpex  7746  unexbOLD  7748  fvclex  7957  naddcllem  8663  ralxpmap  8895  unen  9043  undom  9054  enfixsn  9075  sbthlem10  9085  dif1en  9147  findcard2  9150  unxpdomlem3  9219  isinf  9226  ac6sfi  9245  pwfilem  9278  cnfcomlem  9669  trcl  9698  tc2  9710  rankxpu  9849  rankxplim  9852  rankxplim3  9854  r0weon  9997  infxpenlem  9998  dfac4  10107  dfac2b  10115  kmlem2  10136  cfsmolem  10255  isfin1-3  10371  axdc2lem  10433  axdc3lem4  10438  axcclem  10442  ttukeylem3  10496  gchac  10667  wunex2  10724  wuncval2  10733  inar1  10761  nn0ex  12511  xrex  13012  seqexw  14055  hashbclem  14491  incexclem  15892  ramub1lem2  17088  prdsval  17509  imasval  17566  ipoval  18587  plusffval  18705  smndex1bas  18969  smndex1sgrp  18971  smndex1mnd  18973  smndex1id  18974  grpinvfval  19046  grpsubfval  19051  mulgfval  19136  staffval  20925  scaffval  20982  lpival  21473  cnfldex  21506  xrsex  21520  ipffval  21779  islindf4  21969  psrval  22046  neitr  23318  leordtval2  23350  comppfsc  23670  1stckgen  23692  dfac14  23756  ptcmpfi  23951  hausflim  24119  flimclslem  24122  alexsubALTlem2  24186  nmfval  24726  icccmplem2  24962  tcphex  25357  tchnmfval  25368  taylfval  26500  lrrecse  28113  addsval  28133  negsval  28196  negsid  28212  mulsval  28280  mulsproplem9  28295  precsexlem4  28381  precsexlem5  28382  oncutlt  28435  onaddscl  28448  legval  28831  axlowdimlem15  29284  axlowdim  29289  eengv  29307  uhgrunop  29403  upgrunop  29447  umgrunop  29449  padct  33041  cycpmconjslem2  33453  rlocbas  33566  rlocaddval  33567  rlocmulval  33568  idlsrgval  33771  ordtconnlem1  34292  sxbrsigalem2  34654  actfunsnf1o  34969  actfunsnrndisj  34970  reprsuc  34980  breprexplema  34995  bnj918  35133  fineqvac  35507  subfacp1lem3  35652  subfacp1lem5  35654  erdszelem8  35668  satfvsuclem1  35829  satf0suc  35846  fmlasuc0  35854  mrexval  35971  mrsubcv  35980  mrsubff  35982  mrsubccat  35988  elmrsubrn  35990  dfttc4lem2  37018  rdgssun  38002  exrecfnlem  38003  finixpnum  38234  poimirlem4  38253  poimirlem15  38264  poimirlem28  38277  rrnval  38456  lsatset  39742  ldualset  39877  pclfinN  40652  dvaset  41757  dvhset  41833  hlhilset  42686  evlselv  43301  elrfi  43405  istopclsd  43411  mzpcompact2lem  43462  eldioph2lem1  43471  eldioph2lem2  43472  eldioph4b  43518  diophren  43520  ttac  43743  pwslnmlem2  43800  dfacbasgrp  43815  mendval  43886  idomsubgmo  43900  superuncl  44274  ssuncl  44276  sssymdifcl  44278  rclexi  44321  trclexi  44326  rtrclexi  44327  dfrtrcl5  44335  dfrcl2  44380  comptiunov2i  44412  cotrclrcl  44448  frege83  44652  frege110  44679  frege133  44702  clsk1indlem3  44749  permaxinf2lem  45701  fnchoice  45729  limcresiooub  46336  limcresioolb  46337  fourierdlem48  46848  fourierdlem49  46849  fourierdlem102  46902  fourierdlem114  46914  sge0resplit  47100  elpglem2  50467