Theorem unex 7746

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 4922	. 2 ⊢ ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵)
4		prex 5430	. . 3 ⊢ {𝐴, 𝐵} ∈ V
5	4	uniex 7744	. 2 ⊢ ∪ {𝐴, 𝐵} ∈ V
6	3, 5	eqeltrri 2823	1 ⊢ (𝐴 ∪ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2099  Vcvv 3462   ∪ cun 3944  {cpr 4625  ∪ cuni 4905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5296  ax-nul 5303  ax-pr 5425  ax-un 7738

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-dif 3949  df-un 3951  df-ss 3963  df-nul 4323  df-sn 4624  df-pr 4626  df-uni 4906

This theorem is referenced by:  tpex  7747  unexb  7748  fvclex  7964  naddcllem  8698  ralxpmap  8917  unen  9076  undom  9089  enfixsn  9111  sbthlem10  9122  dif1en  9190  dif1enOLD  9192  findcard2  9194  unxpdomlem3  9279  isinf  9287  isinfOLD  9288  findcard2OLD  9311  ac6sfi  9314  pwfilem  9351  pwfilemOLD  9383  cnfcomlem  9735  trcl  9764  tc2  9778  rankxpu  9912  rankxplim  9915  rankxplim3  9917  r0weon  10048  infxpenlem  10049  dfac4  10158  dfac2b  10166  kmlem2  10187  cfsmolem  10304  isfin1-3  10420  axdc2lem  10482  axdc3lem4  10487  axcclem  10491  ttukeylem3  10545  gchac  10715  wunex2  10772  wuncval2  10781  inar1  10809  nn0ex  12524  xrex  13017  seqexw  14031  hashbclem  14464  incexclem  15835  ramub1lem2  17024  prdsval  17465  imasval  17521  ipoval  18550  plusffval  18634  smndex1bas  18891  smndex1sgrp  18893  smndex1mnd  18895  smndex1id  18896  grpinvfval  18968  grpsubfval  18973  mulgfval  19059  staffval  20816  scaffval  20852  lpival  21309  cnfldex  21342  xrsex  21370  ipffval  21640  islindf4  21832  psrval  21908  neitr  23172  leordtval2  23204  comppfsc  23524  1stckgen  23546  dfac14  23610  ptcmpfi  23805  hausflim  23973  flimclslem  23976  alexsubALTlem2  24040  nmfval  24585  icccmplem2  24827  tcphex  25233  tchnmfval  25244  taylfval  26383  lrrecse  27953  addsval  27973  negsval  28032  negsid  28047  mulsval  28107  mulsproplem9  28122  precsexlem4  28206  precsexlem5  28207  legval  28508  axlowdimlem15  28887  axlowdim  28892  eengv  28910  uhgrunop  29008  upgrunop  29052  umgrunop  29054  padct  32633  cycpmconjslem2  33037  rlocbas  33127  rlocaddval  33128  rlocmulval  33129  idlsrgval  33384  ordtconnlem1  33752  sxbrsigalem2  34133  actfunsnf1o  34463  actfunsnrndisj  34464  reprsuc  34474  breprexplema  34489  bnj918  34624  fineqvac  34946  subfacp1lem3  35023  subfacp1lem5  35025  erdszelem8  35039  satfvsuclem1  35200  satf0suc  35217  fmlasuc0  35225  mrexval  35342  mrsubcv  35351  mrsubff  35353  mrsubccat  35359  elmrsubrn  35361  rdgssun  37098  exrecfnlem  37099  finixpnum  37319  poimirlem4  37338  poimirlem15  37349  poimirlem28  37362  rrnval  37541  lsatset  38701  ldualset  38836  pclfinN  39612  dvaset  40717  dvhset  40793  hlhilset  41646  evlselv  42277  elrfi  42388  istopclsd  42394  mzpcompact2lem  42445  eldioph2lem1  42454  eldioph2lem2  42455  eldioph4b  42505  diophren  42507  ttac  42731  pwslnmlem2  42791  dfacbasgrp  42806  mendval  42881  idomsubgmo  42895  superuncl  43272  ssuncl  43274  sssymdifcl  43276  rclexi  43319  trclexi  43324  rtrclexi  43325  dfrtrcl5  43333  dfrcl2  43378  comptiunov2i  43410  cotrclrcl  43446  frege83  43650  frege110  43677  frege133  43700  clsk1indlem3  43747  fnchoice  44665  limcresiooub  45299  limcresioolb  45300  fourierdlem48  45811  fourierdlem49  45812  fourierdlem102  45865  fourierdlem114  45877  sge0resplit  46063  elpglem2  48494