Theorem unex 7733

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 4927	. 2 ⊢ ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵)
4		prex 5433	. . 3 ⊢ {𝐴, 𝐵} ∈ V
5	4	uniex 7731	. 2 ⊢ ∪ {𝐴, 𝐵} ∈ V
6	3, 5	eqeltrri 2831	1 ⊢ (𝐴 ∪ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2107  Vcvv 3475   ∪ cun 3947  {cpr 4631  ∪ cuni 4909

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-sn 4630  df-pr 4632  df-uni 4910

This theorem is referenced by:  tpex  7734  unexb  7735  fvclex  7945  naddcllem  8675  ralxpmap  8890  unen  9046  undom  9059  enfixsn  9081  sbthlem10  9092  dif1en  9160  dif1enOLD  9162  findcard2  9164  pwfilem  9177  unxpdomlem3  9252  isinf  9260  isinfOLD  9261  findcard2OLD  9284  ac6sfi  9287  pwfilemOLD  9346  cnfcomlem  9694  trcl  9723  tc2  9737  rankxpu  9871  rankxplim  9874  rankxplim3  9876  r0weon  10007  infxpenlem  10008  dfac4  10117  dfac2b  10125  kmlem2  10146  cfsmolem  10265  isfin1-3  10381  axdc2lem  10443  axdc3lem4  10448  axcclem  10452  ttukeylem3  10506  gchac  10676  wunex2  10733  wuncval2  10742  inar1  10770  nn0ex  12478  xrex  12971  seqexw  13982  hashbclem  14411  incexclem  15782  ramub1lem2  16960  prdsval  17401  imasval  17457  ipoval  18483  plusffval  18567  smndex1bas  18787  smndex1sgrp  18789  smndex1mnd  18791  smndex1id  18792  grpinvfval  18863  grpsubfval  18868  mulgfval  18952  staffval  20455  scaffval  20490  lpival  20883  xrsex  20960  ipffval  21201  islindf4  21393  psrval  21468  neitr  22684  leordtval2  22716  comppfsc  23036  1stckgen  23058  dfac14  23122  ptcmpfi  23317  hausflim  23485  flimclslem  23488  alexsubALTlem2  23552  nmfval  24097  icccmplem2  24339  tcphex  24734  tchnmfval  24745  taylfval  25871  lrrecse  27426  addsval  27446  negsval  27500  negsid  27515  mulsval  27565  mulsproplem9  27580  precsexlem4  27656  precsexlem5  27657  legval  27835  axlowdimlem15  28214  axlowdim  28219  eengv  28237  uhgrunop  28335  upgrunop  28379  umgrunop  28381  padct  31944  cycpmconjslem2  32314  idlsrgval  32617  ordtconnlem1  32904  sxbrsigalem2  33285  actfunsnf1o  33616  actfunsnrndisj  33617  reprsuc  33627  breprexplema  33642  bnj918  33777  fineqvac  34097  subfacp1lem3  34173  subfacp1lem5  34175  erdszelem8  34189  satfvsuclem1  34350  satf0suc  34367  fmlasuc0  34375  mrexval  34492  mrsubcv  34501  mrsubff  34503  mrsubccat  34509  elmrsubrn  34511  gg-cnfldex  35180  rdgssun  36259  exrecfnlem  36260  finixpnum  36473  poimirlem4  36492  poimirlem15  36503  poimirlem28  36516  rrnval  36695  lsatset  37860  ldualset  37995  pclfinN  38771  dvaset  39876  dvhset  39952  hlhilset  40805  evlselv  41159  elrfi  41432  istopclsd  41438  mzpcompact2lem  41489  eldioph2lem1  41498  eldioph2lem2  41499  eldioph4b  41549  diophren  41551  ttac  41775  pwslnmlem2  41835  dfacbasgrp  41850  mendval  41925  idomsubgmo  41940  superuncl  42319  ssuncl  42321  sssymdifcl  42323  rclexi  42366  trclexi  42371  rtrclexi  42372  dfrtrcl5  42380  dfrcl2  42425  comptiunov2i  42457  cotrclrcl  42493  frege83  42697  frege110  42724  frege133  42747  clsk1indlem3  42794  fnchoice  43713  limcresiooub  44358  limcresioolb  44359  fourierdlem48  44870  fourierdlem49  44871  fourierdlem102  44924  fourierdlem114  44936  sge0resplit  45122  elpglem2  47757