Theorem unex 7333

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 4764	. 2 ⊢ ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵)
4		prex 5231	. . 3 ⊢ {𝐴, 𝐵} ∈ V
5	4	uniex 7330	. 2 ⊢ ∪ {𝐴, 𝐵} ∈ V
6	3, 5	eqeltrri 2882	1 ⊢ (𝐴 ∪ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2083  Vcvv 3440   ∪ cun 3863  {cpr 4480  ∪ cuni 4751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pr 5228  ax-un 7326

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-rex 3113  df-v 3442  df-dif 3868  df-un 3870  df-nul 4218  df-sn 4479  df-pr 4481  df-uni 4752

This theorem is referenced by:  tpex  7334  unexb  7335  fvclex  7523  ralxpmap  8316  unen  8451  enfixsn  8480  sbthlem10  8490  unxpdomlem3  8577  isinf  8584  findcard2  8611  ac6sfi  8615  pwfilem  8671  fiin  8739  cnfcomlem  9015  trcl  9023  tc2  9037  rankxpu  9158  rankxplim  9161  rankxplim3  9163  r0weon  9291  infxpenlem  9292  dfac4  9401  dfac2b  9409  kmlem2  9430  cfsmolem  9545  isfin1-3  9661  axdc2lem  9723  axdc3lem4  9728  axcclem  9732  ttukeylem3  9786  gchac  9956  wunex2  10013  wuncval2  10022  inar1  10050  nn0ex  11757  xrex  12240  seqexw  13239  hashbclem  13662  incexclem  15028  ramub1lem2  16196  prdsval  16561  imasval  16617  ipoval  17597  fpwipodrs  17607  plusffval  17690  grpinvfval  17903  grpsubfval  17908  mulgfval  17987  staffval  19312  scaffval  19346  lpival  19711  psrval  19834  xrsex  20246  ipffval  20478  islindf4  20668  neitr  21476  leordtval2  21508  comppfsc  21828  1stckgen  21850  dfac14  21914  ptcmpfi  22109  hausflim  22277  flimclslem  22280  alexsubALTlem2  22344  nmfval  22885  icccmplem2  23118  tcphex  23507  tchnmfval  23518  taylfval  24634  legval  26056  axlowdimlem15  26429  axlowdim  26434  eengv  26452  uhgrunop  26547  upgrunop  26591  umgrunop  26593  padct  30139  cycpmconjslem2  30431  ordtconnlem1  30780  sxbrsigalem2  31157  actfunsnf1o  31488  actfunsnrndisj  31489  reprsuc  31499  breprexplema  31514  bnj918  31650  subfacp1lem3  32039  subfacp1lem5  32041  erdszelem8  32055  satfvsuclem1  32216  satf0suc  32233  fmlasuc0  32241  mrexval  32358  mrsubcv  32367  mrsubff  32369  mrsubccat  32375  elmrsubrn  32377  rdgssun  34211  exrecfnlem  34212  finixpnum  34429  poimirlem4  34448  poimirlem15  34459  poimirlem28  34472  rrnval  34658  lsatset  35678  ldualset  35813  pclfinN  36588  dvaset  37693  dvhset  37769  hlhilset  38622  elrfi  38797  istopclsd  38803  mzpcompact2lem  38854  eldioph2lem1  38863  eldioph2lem2  38864  eldioph4b  38914  diophren  38916  ttac  39139  pwslnmlem2  39199  dfacbasgrp  39214  mendval  39289  idomsubgmo  39304  superuncl  39433  ssuncl  39435  sssymdifcl  39437  rclexi  39481  trclexi  39486  rtrclexi  39487  dfrtrcl5  39495  dfrcl2  39525  comptiunov2i  39557  cotrclrcl  39593  frege83  39798  frege110  39825  frege133  39848  clsk1indlem3  39899  isotone1  39904  fnchoice  40846  limcresiooub  41486  limcresioolb  41487  fourierdlem48  42003  fourierdlem49  42004  fourierdlem102  42057  fourierdlem114  42069  sge0resplit  42252  elpglem2  44316