Theorem unex 7509

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 4823	. 2 ⊢ ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵)
4		prex 5310	. . 3 ⊢ {𝐴, 𝐵} ∈ V
5	4	uniex 7507	. 2 ⊢ ∪ {𝐴, 𝐵} ∈ V
6	3, 5	eqeltrri 2828	1 ⊢ (𝐴 ∪ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2112  Vcvv 3398   ∪ cun 3851  {cpr 4529  ∪ cuni 4805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307  ax-un 7501

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-sn 4528  df-pr 4530  df-uni 4806

This theorem is referenced by:  tpex  7510  unexb  7511  fvclex  7710  ralxpmap  8555  unen  8701  enfixsn  8732  sbthlem10  8743  dif1en  8818  findcard2  8820  pwfilem  8832  unxpdomlem3  8860  isinf  8867  findcard2OLD  8891  ac6sfi  8893  pwfilemOLD  8948  cnfcomlem  9292  trcl  9322  tc2  9336  rankxpu  9457  rankxplim  9460  rankxplim3  9462  r0weon  9591  infxpenlem  9592  dfac4  9701  dfac2b  9709  kmlem2  9730  cfsmolem  9849  isfin1-3  9965  axdc2lem  10027  axdc3lem4  10032  axcclem  10036  ttukeylem3  10090  gchac  10260  wunex2  10317  wuncval2  10326  inar1  10354  nn0ex  12061  xrex  12548  seqexw  13555  hashbclem  13981  incexclem  15363  ramub1lem2  16543  prdsval  16914  imasval  16970  ipoval  17990  plusffval  18074  smndex1bas  18287  smndex1sgrp  18289  smndex1mnd  18291  smndex1id  18292  grpinvfval  18360  grpsubfval  18365  mulgfval  18444  staffval  19837  scaffval  19871  lpival  20237  xrsex  20332  ipffval  20564  islindf4  20754  psrval  20828  neitr  22031  leordtval2  22063  comppfsc  22383  1stckgen  22405  dfac14  22469  ptcmpfi  22664  hausflim  22832  flimclslem  22835  alexsubALTlem2  22899  nmfval  23440  icccmplem2  23674  tcphex  24068  tchnmfval  24079  taylfval  25205  legval  26629  axlowdimlem15  27001  axlowdim  27006  eengv  27024  uhgrunop  27120  upgrunop  27164  umgrunop  27166  padct  30728  cycpmconjslem2  31095  idlsrgval  31316  ordtconnlem1  31542  sxbrsigalem2  31919  actfunsnf1o  32250  actfunsnrndisj  32251  reprsuc  32261  breprexplema  32276  bnj918  32412  fineqvac  32733  subfacp1lem3  32811  subfacp1lem5  32813  erdszelem8  32827  satfvsuclem1  32988  satf0suc  33005  fmlasuc0  33013  mrexval  33130  mrsubcv  33139  mrsubff  33141  mrsubccat  33147  elmrsubrn  33149  naddcllem  33517  lrrecse  33785  negsval  33809  addsval  33812  rdgssun  35235  exrecfnlem  35236  finixpnum  35448  poimirlem4  35467  poimirlem15  35478  poimirlem28  35491  rrnval  35671  lsatset  36690  ldualset  36825  pclfinN  37600  dvaset  38705  dvhset  38781  hlhilset  39634  elrfi  40160  istopclsd  40166  mzpcompact2lem  40217  eldioph2lem1  40226  eldioph2lem2  40227  eldioph4b  40277  diophren  40279  ttac  40502  pwslnmlem2  40562  dfacbasgrp  40577  mendval  40652  idomsubgmo  40667  superuncl  40792  ssuncl  40794  sssymdifcl  40796  rclexi  40840  trclexi  40845  rtrclexi  40846  dfrtrcl5  40854  dfrcl2  40900  comptiunov2i  40932  cotrclrcl  40968  frege83  41172  frege110  41199  frege133  41222  clsk1indlem3  41271  fnchoice  42186  limcresiooub  42801  limcresioolb  42802  fourierdlem48  43313  fourierdlem49  43314  fourierdlem102  43367  fourierdlem114  43379  sge0resplit  43562  elpglem2  46031