Theorem unex 6854

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	. . 3 ⊢ 𝐴 ∈ V
2		unex.2	. . 3 ⊢ 𝐵 ∈ V
3	1, 2	unipr 4385	. 2 ⊢ ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵)
4		prex 4836	. . 3 ⊢ {𝐴, 𝐵} ∈ V
5	4	uniex 6851	. 2 ⊢ ∪ {𝐴, 𝐵} ∈ V
6	3, 5	eqeltrri 2685	1 ⊢ (𝐴 ∪ 𝐵) ∈ V

Syntax hints:   ∈ wcel 1977  Vcvv 3173   ∪ cun 3538  {cpr 4127  ∪ cuni 4372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-v 3175  df-dif 3543  df-un 3545  df-nul 3875  df-sn 4126  df-pr 4128  df-uni 4373

This theorem is referenced by:  tpex  6855  unexb  6856  fvclex  7031  ralxpmap  7793  unen  7925  enfixsn  7954  sbthlem10  7964  unxpdomlem3  8051  isinf  8058  findcard2  8085  ac6sfi  8089  pwfilem  8143  fiin  8211  cnfcomlem  8479  trcl  8487  tc2  8501  rankxpu  8622  rankxplim  8625  rankxplim3  8627  r0weon  8718  infxpenlem  8719  dfac4  8828  dfac2  8836  kmlem2  8856  cdafn  8874  cfsmolem  8975  isfin1-3  9091  axdc2lem  9153  axdc3lem4  9158  axcclem  9162  ttukeylem3  9216  gchac  9382  wunex2  9439  wuncval2  9448  inar1  9476  nn0ex  11175  xrex  11705  hashbclem  13093  incexclem  14407  ramub1lem2  15569  prdsval  15938  imasval  15994  ipoval  16977  fpwipodrs  16987  plusffval  17070  staffval  18670  scaffval  18704  lpival  19066  psrval  19183  xrsex  19580  ipffval  19812  islindf4  19996  neitr  20794  leordtval2  20826  comppfsc  21145  1stckgen  21167  dfac14  21231  ptcmpfi  21426  hausflim  21595  flimclslem  21598  alexsubALTlem2  21662  nmfval  22203  icccmplem2  22434  tchex  22824  tchnmfval  22835  taylfval  23917  legval  25279  axlowdimlem15  25636  axlowdim  25641  eengv  25659  uhgrunop  25741  upgrunop  25785  umgrunop  25787  constr3lem1  26173  constr3cyclpe  26191  3v3e3cycl2  26192  padct  28885  ordtconlem1  29298  sxbrsigalem2  29675  bnj918  30090  subfacp1lem3  30418  subfacp1lem5  30420  erdszelem8  30434  mrexval  30652  mrsubcv  30661  mrsubff  30663  mrsubccat  30669  elmrsubrn  30671  finixpnum  32564  poimirlem4  32583  poimirlem15  32594  poimirlem28  32607  rrnval  32796  lsatset  33295  ldualset  33430  pclfinN  34204  dvaset  35311  dvhset  35388  hlhilset  36244  elrfi  36275  istopclsd  36281  mzpcompact2lem  36332  eldioph2lem1  36341  eldioph2lem2  36342  eldioph4b  36393  diophren  36395  ttac  36621  pwslnmlem2  36681  dfacbasgrp  36697  mendval  36772  idomsubgmo  36795  superuncl  36892  ssuncl  36894  sssymdifcl  36896  rclexi  36941  trclexi  36946  rtrclexi  36947  dfrtrcl5  36955  dfrcl2  36985  comptiunov2i  37017  cotrclrcl  37053  frege83  37260  frege110  37287  frege133  37310  clsk1indlem3  37361  isotone1  37366  fnchoice  38211  limcresiooub  38709  limcresioolb  38710  fourierdlem48  39047  fourierdlem49  39048  fourierdlem102  39101  fourierdlem114  39113  sge0resplit  39299  elpglem2  42254