Theorem unex 7755

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

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3458   ∪ cun 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409  ax-un 7745

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-ss 3925  df-sn 4595  df-pr 4597  df-uni 4878

This theorem is used by:  tpex  7756  fvclex  7965  naddcllem  8671  ralxpmap  8903  unen  9052  undom  9063  enfixsn  9084  sbthlem10  9094  dif1en  9156  findcard2  9159  unxpdomlem3  9228  isinf  9235  ac6sfi  9254  pwfilem  9287  cnfcomlem  9678  trcl  9707  tc2  9719  rankxpu  9858  rankxplim  9861  rankxplim3  9863  r0weon  10015  infxpenlem  10016  dfac4  10125  dfac2b  10133  kmlem2  10154  cfsmolem  10272  isfin1-3  10388  axdc2lem  10450  axdc3lem4  10455  axcclem  10459  ttukeylem3  10513  gchac  10684  wunex2  10741  wuncval2  10750  inar1  10778  nn0ex  12528  xrex  13029  seqexw  14073  hashbclem  14509  incexclem  15916  ramub1lem2  17112  prdsval  17533  imasval  17590  ipoval  18611  plusffval  18729  smndex1bas  18999  smndex1sgrp  19001  smndex1mnd  19003  smndex1id  19004  grpinvfval  19076  grpsubfval  19081  mulgfval  19166  staffval  20981  scaffval  21038  lpival  21529  cnfldex  21562  xrsex  21576  ipffval  21835  islindf4  22025  psrval  22102  neitr  23374  leordtval2  23406  comppfsc  23726  1stckgen  23748  dfac14  23812  ptcmpfi  24007  hausflim  24175  flimclslem  24178  alexsubALTlem2  24242  nmfval  24782  icccmplem2  25018  tcphex  25413  tchnmfval  25424  taylfval  26559  lrrecse  28172  addsval  28192  negsval  28255  negsid  28271  mulsval  28339  mulsproplem9  28354  precsexlem4  28440  precsexlem5  28441  oncutlt  28494  onaddscl  28507  legval  28890  axlowdimlem15  29343  axlowdim  29348  eengv  29366  uhgrunop  29462  upgrunop  29506  umgrunop  29508  padct  33100  cycpmconjslem2  33506  rlocbas  33619  rlocaddval  33620  rlocmulval  33621  idlsrgval  33824  ordtconnlem1  34345  sxbrsigalem2  34708  actfunsnf1o  35023  actfunsnrndisj  35024  reprsuc  35034  breprexplema  35049  bnj918  35187  fineqvac  35553  subfacp1lem3  35695  subfacp1lem5  35697  erdszelem8  35711  satfvsuclem1  35872  satf0suc  35889  fmlasuc0  35897  mrexval  36014  mrsubcv  36023  mrsubff  36025  mrsubccat  36031  elmrsubrn  36033  dfttc4lem2  37081  rdgssun  38065  exrecfnlem  38066  finixpnum  38297  poimirlem4  38316  poimirlem15  38327  poimirlem28  38340  rrnval  38519  lsatset  39805  ldualset  39940  pclfinN  40715  dvaset  41820  dvhset  41896  hlhilset  42749  evlselv  43362  elrfi  43466  istopclsd  43472  mzpcompact2lem  43523  eldioph2lem1  43532  eldioph2lem2  43533  eldioph4b  43579  diophren  43581  ttac  43804  pwslnmlem2  43861  dfacbasgrp  43876  mendval  43947  idomsubgmo  43961  superuncl  44335  ssuncl  44337  sssymdifcl  44339  rclexi  44382  trclexi  44387  rtrclexi  44388  dfrtrcl5  44396  dfrcl2  44441  comptiunov2i  44473  cotrclrcl  44509  frege83  44713  frege110  44740  frege133  44763  clsk1indlem3  44810  permaxinf2lem  45762  fnchoice  45790  limcresiooub  46397  limcresioolb  46398  fourierdlem48  46909  fourierdlem49  46910  fourierdlem102  46963  fourierdlem114  46975  sge0resplit  47161  elpglem2  50531