Theorem unex 7596

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 4857	. 2 ⊢ ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵)
4		prex 5355	. . 3 ⊢ {𝐴, 𝐵} ∈ V
5	4	uniex 7594	. 2 ⊢ ∪ {𝐴, 𝐵} ∈ V
6	3, 5	eqeltrri 2836	1 ⊢ (𝐴 ∪ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2106  Vcvv 3432   ∪ cun 3885  {cpr 4563  ∪ cuni 4839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-sn 4562  df-pr 4564  df-uni 4840

This theorem is referenced by:  tpex  7597  unexb  7598  fvclex  7801  ralxpmap  8684  unen  8836  undom  8846  enfixsn  8868  sbthlem10  8879  dif1en  8945  findcard2  8947  pwfilem  8960  unxpdomlem3  9029  isinf  9036  findcard2OLD  9056  ac6sfi  9058  pwfilemOLD  9113  cnfcomlem  9457  trcl  9486  tc2  9500  rankxpu  9634  rankxplim  9637  rankxplim3  9639  r0weon  9768  infxpenlem  9769  dfac4  9878  dfac2b  9886  kmlem2  9907  cfsmolem  10026  isfin1-3  10142  axdc2lem  10204  axdc3lem4  10209  axcclem  10213  ttukeylem3  10267  gchac  10437  wunex2  10494  wuncval2  10503  inar1  10531  nn0ex  12239  xrex  12727  seqexw  13737  hashbclem  14164  incexclem  15548  ramub1lem2  16728  prdsval  17166  imasval  17222  ipoval  18248  plusffval  18332  smndex1bas  18545  smndex1sgrp  18547  smndex1mnd  18549  smndex1id  18550  grpinvfval  18618  grpsubfval  18623  mulgfval  18702  staffval  20107  scaffval  20141  lpival  20516  xrsex  20613  ipffval  20853  islindf4  21045  psrval  21118  neitr  22331  leordtval2  22363  comppfsc  22683  1stckgen  22705  dfac14  22769  ptcmpfi  22964  hausflim  23132  flimclslem  23135  alexsubALTlem2  23199  nmfval  23744  icccmplem2  23986  tcphex  24381  tchnmfval  24392  taylfval  25518  legval  26945  axlowdimlem15  27324  axlowdim  27329  eengv  27347  uhgrunop  27445  upgrunop  27489  umgrunop  27491  padct  31054  cycpmconjslem2  31422  idlsrgval  31648  ordtconnlem1  31874  sxbrsigalem2  32253  actfunsnf1o  32584  actfunsnrndisj  32585  reprsuc  32595  breprexplema  32610  bnj918  32746  fineqvac  33066  subfacp1lem3  33144  subfacp1lem5  33146  erdszelem8  33160  satfvsuclem1  33321  satf0suc  33338  fmlasuc0  33346  mrexval  33463  mrsubcv  33472  mrsubff  33474  mrsubccat  33480  elmrsubrn  33482  naddcllem  33831  lrrecse  34099  negsval  34123  addsval  34126  rdgssun  35549  exrecfnlem  35550  finixpnum  35762  poimirlem4  35781  poimirlem15  35792  poimirlem28  35805  rrnval  35985  lsatset  37004  ldualset  37139  pclfinN  37914  dvaset  39019  dvhset  39095  hlhilset  39948  elrfi  40516  istopclsd  40522  mzpcompact2lem  40573  eldioph2lem1  40582  eldioph2lem2  40583  eldioph4b  40633  diophren  40635  ttac  40858  pwslnmlem2  40918  dfacbasgrp  40933  mendval  41008  idomsubgmo  41023  superuncl  41175  ssuncl  41177  sssymdifcl  41179  rclexi  41223  trclexi  41228  rtrclexi  41229  dfrtrcl5  41237  dfrcl2  41282  comptiunov2i  41314  cotrclrcl  41350  frege83  41554  frege110  41581  frege133  41604  clsk1indlem3  41653  fnchoice  42572  limcresiooub  43183  limcresioolb  43184  fourierdlem48  43695  fourierdlem49  43696  fourierdlem102  43749  fourierdlem114  43761  sge0resplit  43944  elpglem2  46417