Theorem unex 7723

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

Syntax hints:   ∈ wcel 2109  Vcvv 3450   ∪ cun 3915

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-sn 4593  df-pr 4595  df-uni 4875

This theorem is referenced by:  tpex  7725  unexbOLD  7727  fvclex  7940  naddcllem  8643  ralxpmap  8872  unen  9020  undom  9033  enfixsn  9055  sbthlem10  9066  dif1en  9130  dif1enOLD  9132  findcard2  9134  unxpdomlem3  9206  isinf  9214  isinfOLD  9215  ac6sfi  9238  pwfilem  9274  cnfcomlem  9659  trcl  9688  tc2  9702  rankxpu  9836  rankxplim  9839  rankxplim3  9841  r0weon  9972  infxpenlem  9973  dfac4  10082  dfac2b  10091  kmlem2  10112  cfsmolem  10230  isfin1-3  10346  axdc2lem  10408  axdc3lem4  10413  axcclem  10417  ttukeylem3  10471  gchac  10641  wunex2  10698  wuncval2  10707  inar1  10735  nn0ex  12455  xrex  12953  seqexw  13989  hashbclem  14424  incexclem  15809  ramub1lem2  17005  prdsval  17425  imasval  17481  ipoval  18496  plusffval  18580  smndex1bas  18840  smndex1sgrp  18842  smndex1mnd  18844  smndex1id  18845  grpinvfval  18917  grpsubfval  18922  mulgfval  19008  staffval  20757  scaffval  20793  lpival  21241  cnfldex  21274  xrsex  21301  ipffval  21564  islindf4  21754  psrval  21831  neitr  23074  leordtval2  23106  comppfsc  23426  1stckgen  23448  dfac14  23512  ptcmpfi  23707  hausflim  23875  flimclslem  23878  alexsubALTlem2  23942  nmfval  24483  icccmplem2  24719  tcphex  25124  tchnmfval  25135  taylfval  26273  lrrecse  27856  addsval  27876  negsval  27938  negsid  27954  mulsval  28019  mulsproplem9  28034  precsexlem4  28119  precsexlem5  28120  onscutlt  28172  onaddscl  28181  legval  28518  axlowdimlem15  28890  axlowdim  28895  eengv  28913  uhgrunop  29009  upgrunop  29053  umgrunop  29055  padct  32650  cycpmconjslem2  33119  rlocbas  33225  rlocaddval  33226  rlocmulval  33227  idlsrgval  33481  ordtconnlem1  33921  sxbrsigalem2  34284  actfunsnf1o  34602  actfunsnrndisj  34603  reprsuc  34613  breprexplema  34628  bnj918  34763  fineqvac  35094  subfacp1lem3  35176  subfacp1lem5  35178  erdszelem8  35192  satfvsuclem1  35353  satf0suc  35370  fmlasuc0  35378  mrexval  35495  mrsubcv  35504  mrsubff  35506  mrsubccat  35512  elmrsubrn  35514  rdgssun  37373  exrecfnlem  37374  finixpnum  37606  poimirlem4  37625  poimirlem15  37636  poimirlem28  37649  rrnval  37828  lsatset  38990  ldualset  39125  pclfinN  39901  dvaset  41006  dvhset  41082  hlhilset  41935  evlselv  42582  elrfi  42689  istopclsd  42695  mzpcompact2lem  42746  eldioph2lem1  42755  eldioph2lem2  42756  eldioph4b  42806  diophren  42808  ttac  43032  pwslnmlem2  43089  dfacbasgrp  43104  mendval  43175  idomsubgmo  43189  superuncl  43564  ssuncl  43566  sssymdifcl  43568  rclexi  43611  trclexi  43616  rtrclexi  43617  dfrtrcl5  43625  dfrcl2  43670  comptiunov2i  43702  cotrclrcl  43738  frege83  43942  frege110  43969  frege133  43992  clsk1indlem3  44039  permaxinf2lem  45009  fnchoice  45030  limcresiooub  45647  limcresioolb  45648  fourierdlem48  46159  fourierdlem49  46160  fourierdlem102  46213  fourierdlem114  46225  sge0resplit  46411  elpglem2  49705