Theorem unex 7729

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 4925	. 2 ⊢ ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵)
4		prex 5431	. . 3 ⊢ {𝐴, 𝐵} ∈ V
5	4	uniex 7727	. 2 ⊢ ∪ {𝐴, 𝐵} ∈ V
6	3, 5	eqeltrri 2830	1 ⊢ (𝐴 ∪ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2106  Vcvv 3474   ∪ cun 3945  {cpr 4629  ∪ cuni 4907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7721

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-sn 4628  df-pr 4630  df-uni 4908

This theorem is referenced by:  tpex  7730  unexb  7731  fvclex  7941  naddcllem  8671  ralxpmap  8886  unen  9042  undom  9055  enfixsn  9077  sbthlem10  9088  dif1en  9156  dif1enOLD  9158  findcard2  9160  pwfilem  9173  unxpdomlem3  9248  isinf  9256  isinfOLD  9257  findcard2OLD  9280  ac6sfi  9283  pwfilemOLD  9342  cnfcomlem  9690  trcl  9719  tc2  9733  rankxpu  9867  rankxplim  9870  rankxplim3  9872  r0weon  10003  infxpenlem  10004  dfac4  10113  dfac2b  10121  kmlem2  10142  cfsmolem  10261  isfin1-3  10377  axdc2lem  10439  axdc3lem4  10444  axcclem  10448  ttukeylem3  10502  gchac  10672  wunex2  10729  wuncval2  10738  inar1  10766  nn0ex  12474  xrex  12967  seqexw  13978  hashbclem  14407  incexclem  15778  ramub1lem2  16956  prdsval  17397  imasval  17453  ipoval  18479  plusffval  18563  smndex1bas  18783  smndex1sgrp  18785  smndex1mnd  18787  smndex1id  18788  grpinvfval  18859  grpsubfval  18864  mulgfval  18946  staffval  20447  scaffval  20482  lpival  20875  xrsex  20952  ipffval  21192  islindf4  21384  psrval  21459  neitr  22675  leordtval2  22707  comppfsc  23027  1stckgen  23049  dfac14  23113  ptcmpfi  23308  hausflim  23476  flimclslem  23479  alexsubALTlem2  23543  nmfval  24088  icccmplem2  24330  tcphex  24725  tchnmfval  24736  taylfval  25862  lrrecse  27415  addsval  27435  negsval  27489  negsid  27504  mulsval  27554  mulsproplem9  27569  precsexlem4  27645  precsexlem5  27646  legval  27824  axlowdimlem15  28203  axlowdim  28208  eengv  28226  uhgrunop  28324  upgrunop  28368  umgrunop  28370  padct  31931  cycpmconjslem2  32301  idlsrgval  32605  ordtconnlem1  32892  sxbrsigalem2  33273  actfunsnf1o  33604  actfunsnrndisj  33605  reprsuc  33615  breprexplema  33630  bnj918  33765  fineqvac  34085  subfacp1lem3  34161  subfacp1lem5  34163  erdszelem8  34177  satfvsuclem1  34338  satf0suc  34355  fmlasuc0  34363  mrexval  34480  mrsubcv  34489  mrsubff  34491  mrsubccat  34497  elmrsubrn  34499  gg-cnfldex  35168  rdgssun  36247  exrecfnlem  36248  finixpnum  36461  poimirlem4  36480  poimirlem15  36491  poimirlem28  36504  rrnval  36683  lsatset  37848  ldualset  37983  pclfinN  38759  dvaset  39864  dvhset  39940  hlhilset  40793  evlselv  41156  elrfi  41417  istopclsd  41423  mzpcompact2lem  41474  eldioph2lem1  41483  eldioph2lem2  41484  eldioph4b  41534  diophren  41536  ttac  41760  pwslnmlem2  41820  dfacbasgrp  41835  mendval  41910  idomsubgmo  41925  superuncl  42304  ssuncl  42306  sssymdifcl  42308  rclexi  42351  trclexi  42356  rtrclexi  42357  dfrtrcl5  42365  dfrcl2  42410  comptiunov2i  42442  cotrclrcl  42478  frege83  42682  frege110  42709  frege133  42732  clsk1indlem3  42779  fnchoice  43698  limcresiooub  44344  limcresioolb  44345  fourierdlem48  44856  fourierdlem49  44857  fourierdlem102  44910  fourierdlem114  44922  sge0resplit  45108  elpglem2  47710