Theorem unex 7469

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 4855	. 2 ⊢ ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵)
4		prex 5333	. . 3 ⊢ {𝐴, 𝐵} ∈ V
5	4	uniex 7467	. 2 ⊢ ∪ {𝐴, 𝐵} ∈ V
6	3, 5	eqeltrri 2910	1 ⊢ (𝐴 ∪ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3494   ∪ cun 3934  {cpr 4569  ∪ cuni 4838

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-sn 4568  df-pr 4570  df-uni 4839

This theorem is referenced by:  tpex  7470  unexb  7471  fvclex  7660  ralxpmap  8460  unen  8596  enfixsn  8626  sbthlem10  8636  unxpdomlem3  8724  isinf  8731  findcard2  8758  ac6sfi  8762  pwfilem  8818  cnfcomlem  9162  trcl  9170  tc2  9184  rankxpu  9305  rankxplim  9308  rankxplim3  9310  r0weon  9438  infxpenlem  9439  dfac4  9548  dfac2b  9556  kmlem2  9577  cfsmolem  9692  isfin1-3  9808  axdc2lem  9870  axdc3lem4  9875  axcclem  9879  ttukeylem3  9933  gchac  10103  wunex2  10160  wuncval2  10169  inar1  10197  nn0ex  11904  xrex  12387  seqexw  13386  hashbclem  13811  incexclem  15191  ramub1lem2  16363  prdsval  16728  imasval  16784  ipoval  17764  plusffval  17858  smndex1bas  18071  smndex1sgrp  18073  smndex1mnd  18075  smndex1id  18076  grpinvfval  18142  grpsubfval  18147  mulgfval  18226  staffval  19618  scaffval  19652  lpival  20018  psrval  20142  xrsex  20560  ipffval  20792  islindf4  20982  neitr  21788  leordtval2  21820  comppfsc  22140  1stckgen  22162  dfac14  22226  ptcmpfi  22421  hausflim  22589  flimclslem  22592  alexsubALTlem2  22656  nmfval  23198  icccmplem2  23431  tcphex  23820  tchnmfval  23831  taylfval  24947  legval  26370  axlowdimlem15  26742  axlowdim  26747  eengv  26765  uhgrunop  26860  upgrunop  26904  umgrunop  26906  padct  30455  cycpmconjslem2  30797  ordtconnlem1  31167  sxbrsigalem2  31544  actfunsnf1o  31875  actfunsnrndisj  31876  reprsuc  31886  breprexplema  31901  bnj918  32037  subfacp1lem3  32429  subfacp1lem5  32431  erdszelem8  32445  satfvsuclem1  32606  satf0suc  32623  fmlasuc0  32631  mrexval  32748  mrsubcv  32757  mrsubff  32759  mrsubccat  32765  elmrsubrn  32767  rdgssun  34662  exrecfnlem  34663  finixpnum  34892  poimirlem4  34911  poimirlem15  34922  poimirlem28  34935  rrnval  35120  lsatset  36141  ldualset  36276  pclfinN  37051  dvaset  38156  dvhset  38232  hlhilset  39085  elrfi  39311  istopclsd  39317  mzpcompact2lem  39368  eldioph2lem1  39377  eldioph2lem2  39378  eldioph4b  39428  diophren  39430  ttac  39653  pwslnmlem2  39713  dfacbasgrp  39728  mendval  39803  idomsubgmo  39818  superuncl  39947  ssuncl  39949  sssymdifcl  39951  rclexi  39995  trclexi  40000  rtrclexi  40001  dfrtrcl5  40009  dfrcl2  40039  comptiunov2i  40071  cotrclrcl  40107  frege83  40312  frege110  40339  frege133  40362  clsk1indlem3  40413  fnchoice  41306  limcresiooub  41943  limcresioolb  41944  fourierdlem48  42459  fourierdlem49  42460  fourierdlem102  42513  fourierdlem114  42525  sge0resplit  42708  elpglem2  44834