Theorem unex 6998

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 4481	. 2 ⊢ ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵)
4		prex 4939	. . 3 ⊢ {𝐴, 𝐵} ∈ V
5	4	uniex 6995	. 2 ⊢ ∪ {𝐴, 𝐵} ∈ V
6	3, 5	eqeltrri 2727	1 ⊢ (𝐴 ∪ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2030  Vcvv 3231   ∪ cun 3605  {cpr 4212  ∪ cuni 4468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936  ax-un 6991

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-v 3233  df-dif 3610  df-un 3612  df-nul 3949  df-sn 4211  df-pr 4213  df-uni 4469

This theorem is referenced by:  tpex  6999  unexb  7000  fvclex  7180  ralxpmap  7949  unen  8081  enfixsn  8110  sbthlem10  8120  unxpdomlem3  8207  isinf  8214  findcard2  8241  ac6sfi  8245  pwfilem  8301  fiin  8369  cnfcomlem  8634  trcl  8642  tc2  8656  rankxpu  8777  rankxplim  8780  rankxplim3  8782  r0weon  8873  infxpenlem  8874  dfac4  8983  dfac2  8991  kmlem2  9011  cdafn  9029  cfsmolem  9130  isfin1-3  9246  axdc2lem  9308  axdc3lem4  9313  axcclem  9317  ttukeylem3  9371  gchac  9541  wunex2  9598  wuncval2  9607  inar1  9635  nn0ex  11336  xrex  11867  hashbclem  13274  incexclem  14612  ramub1lem2  15778  prdsval  16162  imasval  16218  ipoval  17201  fpwipodrs  17211  plusffval  17294  staffval  18895  scaffval  18929  lpival  19293  psrval  19410  xrsex  19809  ipffval  20041  islindf4  20225  neitr  21032  leordtval2  21064  comppfsc  21383  1stckgen  21405  dfac14  21469  ptcmpfi  21664  hausflim  21832  flimclslem  21835  alexsubALTlem2  21899  nmfval  22440  icccmplem2  22673  tchex  23062  tchnmfval  23073  taylfval  24158  legval  25524  axlowdimlem15  25881  axlowdim  25886  eengv  25904  uhgrunop  26015  upgrunop  26059  umgrunop  26061  padct  29625  ordtconnlem1  30098  sxbrsigalem2  30476  actfunsnf1o  30810  actfunsnrndisj  30811  reprsuc  30821  breprexplema  30836  bnj918  30962  subfacp1lem3  31290  subfacp1lem5  31292  erdszelem8  31306  mrexval  31524  mrsubcv  31533  mrsubff  31535  mrsubccat  31541  elmrsubrn  31543  finixpnum  33524  poimirlem4  33543  poimirlem15  33554  poimirlem28  33567  rrnval  33756  lsatset  34595  ldualset  34730  pclfinN  35504  dvaset  36610  dvhset  36687  hlhilset  37543  elrfi  37574  istopclsd  37580  mzpcompact2lem  37631  eldioph2lem1  37640  eldioph2lem2  37641  eldioph4b  37692  diophren  37694  ttac  37920  pwslnmlem2  37980  dfacbasgrp  37995  mendval  38070  idomsubgmo  38093  superuncl  38190  ssuncl  38192  sssymdifcl  38194  rclexi  38239  trclexi  38244  rtrclexi  38245  dfrtrcl5  38253  dfrcl2  38283  comptiunov2i  38315  cotrclrcl  38351  frege83  38557  frege110  38584  frege133  38607  clsk1indlem3  38658  isotone1  38663  fnchoice  39502  limcresiooub  40192  limcresioolb  40193  fourierdlem48  40689  fourierdlem49  40690  fourierdlem102  40743  fourierdlem114  40755  sge0resplit  40941  elpglem2  42783