Theorem unex 7574

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

Syntax hints:   ∈ wcel 2108  Vcvv 3422   ∪ cun 3881  {cpr 4560  ∪ cuni 4836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-sn 4559  df-pr 4561  df-uni 4837

This theorem is referenced by:  tpex  7575  unexb  7576  fvclex  7775  ralxpmap  8642  unen  8790  enfixsn  8821  sbthlem10  8832  dif1en  8907  findcard2  8909  pwfilem  8922  unxpdomlem3  8958  isinf  8965  findcard2OLD  8986  ac6sfi  8988  pwfilemOLD  9043  cnfcomlem  9387  trcl  9417  tc2  9431  rankxpu  9565  rankxplim  9568  rankxplim3  9570  r0weon  9699  infxpenlem  9700  dfac4  9809  dfac2b  9817  kmlem2  9838  cfsmolem  9957  isfin1-3  10073  axdc2lem  10135  axdc3lem4  10140  axcclem  10144  ttukeylem3  10198  gchac  10368  wunex2  10425  wuncval2  10434  inar1  10462  nn0ex  12169  xrex  12656  seqexw  13665  hashbclem  14092  incexclem  15476  ramub1lem2  16656  prdsval  17083  imasval  17139  ipoval  18163  plusffval  18247  smndex1bas  18460  smndex1sgrp  18462  smndex1mnd  18464  smndex1id  18465  grpinvfval  18533  grpsubfval  18538  mulgfval  18617  staffval  20022  scaffval  20056  lpival  20429  xrsex  20525  ipffval  20765  islindf4  20955  psrval  21028  neitr  22239  leordtval2  22271  comppfsc  22591  1stckgen  22613  dfac14  22677  ptcmpfi  22872  hausflim  23040  flimclslem  23043  alexsubALTlem2  23107  nmfval  23650  icccmplem2  23892  tcphex  24286  tchnmfval  24297  taylfval  25423  legval  26849  axlowdimlem15  27227  axlowdim  27232  eengv  27250  uhgrunop  27348  upgrunop  27392  umgrunop  27394  padct  30956  cycpmconjslem2  31324  idlsrgval  31550  ordtconnlem1  31776  sxbrsigalem2  32153  actfunsnf1o  32484  actfunsnrndisj  32485  reprsuc  32495  breprexplema  32510  bnj918  32646  fineqvac  32966  subfacp1lem3  33044  subfacp1lem5  33046  erdszelem8  33060  satfvsuclem1  33221  satf0suc  33238  fmlasuc0  33246  mrexval  33363  mrsubcv  33372  mrsubff  33374  mrsubccat  33380  elmrsubrn  33382  naddcllem  33758  lrrecse  34026  negsval  34050  addsval  34053  rdgssun  35476  exrecfnlem  35477  finixpnum  35689  poimirlem4  35708  poimirlem15  35719  poimirlem28  35732  rrnval  35912  lsatset  36931  ldualset  37066  pclfinN  37841  dvaset  38946  dvhset  39022  hlhilset  39875  elrfi  40432  istopclsd  40438  mzpcompact2lem  40489  eldioph2lem1  40498  eldioph2lem2  40499  eldioph4b  40549  diophren  40551  ttac  40774  pwslnmlem2  40834  dfacbasgrp  40849  mendval  40924  idomsubgmo  40939  superuncl  41064  ssuncl  41066  sssymdifcl  41068  rclexi  41112  trclexi  41117  rtrclexi  41118  dfrtrcl5  41126  dfrcl2  41171  comptiunov2i  41203  cotrclrcl  41239  frege83  41443  frege110  41470  frege133  41493  clsk1indlem3  41542  fnchoice  42461  limcresiooub  43073  limcresioolb  43074  fourierdlem48  43585  fourierdlem49  43586  fourierdlem102  43639  fourierdlem114  43651  sge0resplit  43834  elpglem2  46303