Theorem unex 7638

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 4868	. 2 ⊢ ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵)
4		prex 5370	. . 3 ⊢ {𝐴, 𝐵} ∈ V
5	4	uniex 7636	. 2 ⊢ ∪ {𝐴, 𝐵} ∈ V
6	3, 5	eqeltrri 2835	1 ⊢ (𝐴 ∪ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2105  Vcvv 3441   ∪ cun 3895  {cpr 4573  ∪ cuni 4850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pr 5367  ax-un 7630

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-sn 4572  df-pr 4574  df-uni 4851

This theorem is referenced by:  tpex  7639  unexb  7640  fvclex  7848  ralxpmap  8734  unen  8890  undom  8903  enfixsn  8925  sbthlem10  8936  dif1en  9004  dif1enOLD  9006  findcard2  9008  pwfilem  9021  unxpdomlem3  9096  isinf  9104  isinfOLD  9105  findcard2OLD  9128  ac6sfi  9131  pwfilemOLD  9190  cnfcomlem  9535  trcl  9564  tc2  9578  rankxpu  9712  rankxplim  9715  rankxplim3  9717  r0weon  9848  infxpenlem  9849  dfac4  9958  dfac2b  9966  kmlem2  9987  cfsmolem  10106  isfin1-3  10222  axdc2lem  10284  axdc3lem4  10289  axcclem  10293  ttukeylem3  10347  gchac  10517  wunex2  10574  wuncval2  10583  inar1  10611  nn0ex  12319  xrex  12807  seqexw  13817  hashbclem  14243  incexclem  15627  ramub1lem2  16805  prdsval  17243  imasval  17299  ipoval  18325  plusffval  18409  smndex1bas  18621  smndex1sgrp  18623  smndex1mnd  18625  smndex1id  18626  grpinvfval  18694  grpsubfval  18699  mulgfval  18778  staffval  20190  scaffval  20224  lpival  20599  xrsex  20696  ipffval  20936  islindf4  21128  psrval  21201  neitr  22414  leordtval2  22446  comppfsc  22766  1stckgen  22788  dfac14  22852  ptcmpfi  23047  hausflim  23215  flimclslem  23218  alexsubALTlem2  23282  nmfval  23827  icccmplem2  24069  tcphex  24464  tchnmfval  24475  taylfval  25601  legval  27081  axlowdimlem15  27460  axlowdim  27465  eengv  27483  uhgrunop  27581  upgrunop  27625  umgrunop  27627  padct  31189  cycpmconjslem2  31557  idlsrgval  31787  ordtconnlem1  32014  sxbrsigalem2  32393  actfunsnf1o  32724  actfunsnrndisj  32725  reprsuc  32735  breprexplema  32750  bnj918  32885  fineqvac  33205  subfacp1lem3  33283  subfacp1lem5  33285  erdszelem8  33299  satfvsuclem1  33460  satf0suc  33477  fmlasuc0  33485  mrexval  33602  mrsubcv  33611  mrsubff  33613  mrsubccat  33619  elmrsubrn  33621  naddcllem  33958  lrrecse  34173  negsval  34197  addsval  34200  rdgssun  35621  exrecfnlem  35622  finixpnum  35834  poimirlem4  35853  poimirlem15  35864  poimirlem28  35877  rrnval  36057  lsatset  37224  ldualset  37359  pclfinN  38135  dvaset  39240  dvhset  39316  hlhilset  40169  elrfi  40732  istopclsd  40738  mzpcompact2lem  40789  eldioph2lem1  40798  eldioph2lem2  40799  eldioph4b  40849  diophren  40851  ttac  41075  pwslnmlem2  41135  dfacbasgrp  41150  mendval  41225  idomsubgmo  41240  superuncl  41409  ssuncl  41411  sssymdifcl  41413  rclexi  41457  trclexi  41462  rtrclexi  41463  dfrtrcl5  41471  dfrcl2  41516  comptiunov2i  41548  cotrclrcl  41584  frege83  41788  frege110  41815  frege133  41838  clsk1indlem3  41887  fnchoice  42806  limcresiooub  43433  limcresioolb  43434  fourierdlem48  43945  fourierdlem49  43946  fourierdlem102  43999  fourierdlem114  44011  sge0resplit  44195  elpglem2  46682