Theorem unex 7689

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

Syntax hints:   ∈ wcel 2113  Vcvv 3440   ∪ cun 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-sn 4581  df-pr 4583  df-uni 4864

This theorem is referenced by:  tpex  7691  unexbOLD  7693  fvclex  7903  naddcllem  8604  ralxpmap  8834  unen  8982  undom  8993  enfixsn  9014  sbthlem10  9024  dif1en  9086  findcard2  9089  unxpdomlem3  9158  isinf  9165  ac6sfi  9184  pwfilem  9218  cnfcomlem  9608  trcl  9637  tc2  9649  rankxpu  9788  rankxplim  9791  rankxplim3  9793  r0weon  9922  infxpenlem  9923  dfac4  10032  dfac2b  10041  kmlem2  10062  cfsmolem  10180  isfin1-3  10296  axdc2lem  10358  axdc3lem4  10363  axcclem  10367  ttukeylem3  10421  gchac  10592  wunex2  10649  wuncval2  10658  inar1  10686  nn0ex  12407  xrex  12900  seqexw  13940  hashbclem  14375  incexclem  15759  ramub1lem2  16955  prdsval  17375  imasval  17432  ipoval  18453  plusffval  18571  smndex1bas  18831  smndex1sgrp  18833  smndex1mnd  18835  smndex1id  18836  grpinvfval  18908  grpsubfval  18913  mulgfval  18999  staffval  20774  scaffval  20831  lpival  21279  cnfldex  21312  xrsex  21339  ipffval  21603  islindf4  21793  psrval  21871  neitr  23124  leordtval2  23156  comppfsc  23476  1stckgen  23498  dfac14  23562  ptcmpfi  23757  hausflim  23925  flimclslem  23928  alexsubALTlem2  23992  nmfval  24532  icccmplem2  24768  tcphex  25173  tchnmfval  25184  taylfval  26322  lrrecse  27938  addsval  27958  negsval  28021  negsid  28037  mulsval  28105  mulsproplem9  28120  precsexlem4  28206  precsexlem5  28207  oncutlt  28260  onaddscl  28273  legval  28656  axlowdimlem15  29029  axlowdim  29034  eengv  29052  uhgrunop  29148  upgrunop  29192  umgrunop  29194  padct  32797  cycpmconjslem2  33237  rlocbas  33349  rlocaddval  33350  rlocmulval  33351  idlsrgval  33584  ordtconnlem1  34081  sxbrsigalem2  34443  actfunsnf1o  34761  actfunsnrndisj  34762  reprsuc  34772  breprexplema  34787  bnj918  34922  fineqvac  35272  subfacp1lem3  35376  subfacp1lem5  35378  erdszelem8  35392  satfvsuclem1  35553  satf0suc  35570  fmlasuc0  35578  mrexval  35695  mrsubcv  35704  mrsubff  35706  mrsubccat  35712  elmrsubrn  35714  rdgssun  37579  exrecfnlem  37580  finixpnum  37802  poimirlem4  37821  poimirlem15  37832  poimirlem28  37845  rrnval  38024  lsatset  39246  ldualset  39381  pclfinN  40156  dvaset  41261  dvhset  41337  hlhilset  42190  evlselv  42826  elrfi  42932  istopclsd  42938  mzpcompact2lem  42989  eldioph2lem1  42998  eldioph2lem2  42999  eldioph4b  43049  diophren  43051  ttac  43274  pwslnmlem2  43331  dfacbasgrp  43346  mendval  43417  idomsubgmo  43431  superuncl  43805  ssuncl  43807  sssymdifcl  43809  rclexi  43852  trclexi  43857  rtrclexi  43858  dfrtrcl5  43866  dfrcl2  43911  comptiunov2i  43943  cotrclrcl  43979  frege83  44183  frege110  44210  frege133  44233  clsk1indlem3  44280  permaxinf2lem  45249  fnchoice  45270  limcresiooub  45882  limcresioolb  45883  fourierdlem48  46394  fourierdlem49  46395  fourierdlem102  46448  fourierdlem114  46460  sge0resplit  46646  elpglem2  49953