Theorem unex 7677

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436   ∪ cun 3900

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 2113  ax-9 2121  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370  ax-un 7668

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-sn 4577  df-pr 4579  df-uni 4860

This theorem is referenced by:  tpex  7679  unexbOLD  7681  fvclex  7891  naddcllem  8591  ralxpmap  8820  unen  8967  undom  8978  enfixsn  8999  sbthlem10  9009  dif1en  9071  findcard2  9074  unxpdomlem3  9142  isinf  9149  ac6sfi  9168  pwfilem  9202  cnfcomlem  9589  trcl  9618  tc2  9632  rankxpu  9766  rankxplim  9769  rankxplim3  9771  r0weon  9900  infxpenlem  9901  dfac4  10010  dfac2b  10019  kmlem2  10040  cfsmolem  10158  isfin1-3  10274  axdc2lem  10336  axdc3lem4  10341  axcclem  10345  ttukeylem3  10399  gchac  10569  wunex2  10626  wuncval2  10635  inar1  10663  nn0ex  12384  xrex  12882  seqexw  13921  hashbclem  14356  incexclem  15740  ramub1lem2  16936  prdsval  17356  imasval  17412  ipoval  18433  plusffval  18551  smndex1bas  18811  smndex1sgrp  18813  smndex1mnd  18815  smndex1id  18816  grpinvfval  18888  grpsubfval  18893  mulgfval  18979  staffval  20754  scaffval  20811  lpival  21259  cnfldex  21292  xrsex  21319  ipffval  21583  islindf4  21773  psrval  21850  neitr  23093  leordtval2  23125  comppfsc  23445  1stckgen  23467  dfac14  23531  ptcmpfi  23726  hausflim  23894  flimclslem  23897  alexsubALTlem2  23961  nmfval  24501  icccmplem2  24737  tcphex  25142  tchnmfval  25153  taylfval  26291  lrrecse  27883  addsval  27903  negsval  27965  negsid  27981  mulsval  28046  mulsproplem9  28061  precsexlem4  28146  precsexlem5  28147  onscutlt  28199  onaddscl  28208  legval  28560  axlowdimlem15  28932  axlowdim  28937  eengv  28955  uhgrunop  29051  upgrunop  29095  umgrunop  29097  padct  32696  cycpmconjslem2  33119  rlocbas  33229  rlocaddval  33230  rlocmulval  33231  idlsrgval  33463  ordtconnlem1  33932  sxbrsigalem2  34294  actfunsnf1o  34612  actfunsnrndisj  34613  reprsuc  34623  breprexplema  34638  bnj918  34773  fineqvac  35127  subfacp1lem3  35214  subfacp1lem5  35216  erdszelem8  35230  satfvsuclem1  35391  satf0suc  35408  fmlasuc0  35416  mrexval  35533  mrsubcv  35542  mrsubff  35544  mrsubccat  35550  elmrsubrn  35552  rdgssun  37411  exrecfnlem  37412  finixpnum  37644  poimirlem4  37663  poimirlem15  37674  poimirlem28  37687  rrnval  37866  lsatset  39028  ldualset  39163  pclfinN  39938  dvaset  41043  dvhset  41119  hlhilset  41972  evlselv  42619  elrfi  42726  istopclsd  42732  mzpcompact2lem  42783  eldioph2lem1  42792  eldioph2lem2  42793  eldioph4b  42843  diophren  42845  ttac  43068  pwslnmlem2  43125  dfacbasgrp  43140  mendval  43211  idomsubgmo  43225  superuncl  43600  ssuncl  43602  sssymdifcl  43604  rclexi  43647  trclexi  43652  rtrclexi  43653  dfrtrcl5  43661  dfrcl2  43706  comptiunov2i  43738  cotrclrcl  43774  frege83  43978  frege110  44005  frege133  44028  clsk1indlem3  44075  permaxinf2lem  45044  fnchoice  45065  limcresiooub  45679  limcresioolb  45680  fourierdlem48  46191  fourierdlem49  46192  fourierdlem102  46245  fourierdlem114  46257  sge0resplit  46443  elpglem2  49743