Theorem unex 6956

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 4449	. 2 ⊢ ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵)
4		prex 4909	. . 3 ⊢ {𝐴, 𝐵} ∈ V
5	4	uniex 6953	. 2 ⊢ ∪ {𝐴, 𝐵} ∈ V
6	3, 5	eqeltrri 2698	1 ⊢ (𝐴 ∪ 𝐵) ∈ V

Syntax hints:   ∈ wcel 1990  Vcvv 3200   ∪ cun 3572  {cpr 4179  ∪ cuni 4436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-v 3202  df-dif 3577  df-un 3579  df-nul 3916  df-sn 4178  df-pr 4180  df-uni 4437

This theorem is referenced by:  tpex  6957  unexb  6958  fvclex  7138  ralxpmap  7907  unen  8040  enfixsn  8069  sbthlem10  8079  unxpdomlem3  8166  isinf  8173  findcard2  8200  ac6sfi  8204  pwfilem  8260  fiin  8328  cnfcomlem  8596  trcl  8604  tc2  8618  rankxpu  8739  rankxplim  8742  rankxplim3  8744  r0weon  8835  infxpenlem  8836  dfac4  8945  dfac2  8953  kmlem2  8973  cdafn  8991  cfsmolem  9092  isfin1-3  9208  axdc2lem  9270  axdc3lem4  9275  axcclem  9279  ttukeylem3  9333  gchac  9503  wunex2  9560  wuncval2  9569  inar1  9597  nn0ex  11298  xrex  11829  hashbclem  13236  incexclem  14568  ramub1lem2  15731  prdsval  16115  imasval  16171  ipoval  17154  fpwipodrs  17164  plusffval  17247  staffval  18847  scaffval  18881  lpival  19245  psrval  19362  xrsex  19761  ipffval  19993  islindf4  20177  neitr  20984  leordtval2  21016  comppfsc  21335  1stckgen  21357  dfac14  21421  ptcmpfi  21616  hausflim  21785  flimclslem  21788  alexsubALTlem2  21852  nmfval  22393  icccmplem2  22626  tchex  23016  tchnmfval  23027  taylfval  24113  legval  25479  axlowdimlem15  25836  axlowdim  25841  eengv  25859  uhgrunop  25970  upgrunop  26014  umgrunop  26016  padct  29497  ordtconnlem1  29970  sxbrsigalem2  30348  actfunsnf1o  30682  actfunsnrndisj  30683  reprsuc  30693  breprexplema  30708  bnj918  30836  subfacp1lem3  31164  subfacp1lem5  31166  erdszelem8  31180  mrexval  31398  mrsubcv  31407  mrsubff  31409  mrsubccat  31415  elmrsubrn  31417  finixpnum  33394  poimirlem4  33413  poimirlem15  33424  poimirlem28  33437  rrnval  33626  lsatset  34277  ldualset  34412  pclfinN  35186  dvaset  36293  dvhset  36370  hlhilset  37226  elrfi  37257  istopclsd  37263  mzpcompact2lem  37314  eldioph2lem1  37323  eldioph2lem2  37324  eldioph4b  37375  diophren  37377  ttac  37603  pwslnmlem2  37663  dfacbasgrp  37678  mendval  37753  idomsubgmo  37776  superuncl  37873  ssuncl  37875  sssymdifcl  37877  rclexi  37922  trclexi  37927  rtrclexi  37928  dfrtrcl5  37936  dfrcl2  37966  comptiunov2i  37998  cotrclrcl  38034  frege83  38240  frege110  38267  frege133  38290  clsk1indlem3  38341  isotone1  38346  fnchoice  39188  limcresiooub  39874  limcresioolb  39875  fourierdlem48  40371  fourierdlem49  40372  fourierdlem102  40425  fourierdlem114  40437  sge0resplit  40623  elpglem2  42455