Theorem unex 7779

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	. 2 ⊢ 𝐴 ∈ V
2		unex.2	. 2 ⊢ 𝐵 ∈ V
3		unexg 7778	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∪ 𝐵) ∈ V)
4	1, 2, 3	mp2an 691	1 ⊢ (𝐴 ∪ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3488   ∪ cun 3974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-sn 4649  df-pr 4651  df-uni 4932

This theorem is referenced by:  tpex  7781  unexbOLD  7783  fvclex  7999  naddcllem  8732  ralxpmap  8954  unen  9112  undom  9125  enfixsn  9147  sbthlem10  9158  dif1en  9226  dif1enOLD  9228  findcard2  9230  unxpdomlem3  9315  isinf  9323  isinfOLD  9324  ac6sfi  9348  pwfilem  9384  pwfilemOLD  9416  cnfcomlem  9768  trcl  9797  tc2  9811  rankxpu  9945  rankxplim  9948  rankxplim3  9950  r0weon  10081  infxpenlem  10082  dfac4  10191  dfac2b  10200  kmlem2  10221  cfsmolem  10339  isfin1-3  10455  axdc2lem  10517  axdc3lem4  10522  axcclem  10526  ttukeylem3  10580  gchac  10750  wunex2  10807  wuncval2  10816  inar1  10844  nn0ex  12559  xrex  13052  seqexw  14068  hashbclem  14501  incexclem  15884  ramub1lem2  17074  prdsval  17515  imasval  17571  ipoval  18600  plusffval  18684  smndex1bas  18941  smndex1sgrp  18943  smndex1mnd  18945  smndex1id  18946  grpinvfval  19018  grpsubfval  19023  mulgfval  19109  staffval  20864  scaffval  20900  lpival  21357  cnfldex  21390  xrsex  21418  ipffval  21689  islindf4  21881  psrval  21958  neitr  23209  leordtval2  23241  comppfsc  23561  1stckgen  23583  dfac14  23647  ptcmpfi  23842  hausflim  24010  flimclslem  24013  alexsubALTlem2  24077  nmfval  24622  icccmplem2  24864  tcphex  25270  tchnmfval  25281  taylfval  26418  lrrecse  27993  addsval  28013  negsval  28075  negsid  28091  mulsval  28153  mulsproplem9  28168  precsexlem4  28252  precsexlem5  28253  onaddscl  28304  legval  28610  axlowdimlem15  28989  axlowdim  28994  eengv  29012  uhgrunop  29110  upgrunop  29154  umgrunop  29156  padct  32733  cycpmconjslem2  33148  rlocbas  33239  rlocaddval  33240  rlocmulval  33241  idlsrgval  33496  ordtconnlem1  33870  sxbrsigalem2  34251  actfunsnf1o  34581  actfunsnrndisj  34582  reprsuc  34592  breprexplema  34607  bnj918  34742  fineqvac  35073  subfacp1lem3  35150  subfacp1lem5  35152  erdszelem8  35166  satfvsuclem1  35327  satf0suc  35344  fmlasuc0  35352  mrexval  35469  mrsubcv  35478  mrsubff  35480  mrsubccat  35486  elmrsubrn  35488  rdgssun  37344  exrecfnlem  37345  finixpnum  37565  poimirlem4  37584  poimirlem15  37595  poimirlem28  37608  rrnval  37787  lsatset  38946  ldualset  39081  pclfinN  39857  dvaset  40962  dvhset  41038  hlhilset  41891  evlselv  42542  elrfi  42650  istopclsd  42656  mzpcompact2lem  42707  eldioph2lem1  42716  eldioph2lem2  42717  eldioph4b  42767  diophren  42769  ttac  42993  pwslnmlem2  43050  dfacbasgrp  43065  mendval  43140  idomsubgmo  43154  superuncl  43530  ssuncl  43532  sssymdifcl  43534  rclexi  43577  trclexi  43582  rtrclexi  43583  dfrtrcl5  43591  dfrcl2  43636  comptiunov2i  43668  cotrclrcl  43704  frege83  43908  frege110  43935  frege133  43958  clsk1indlem3  44005  fnchoice  44929  limcresiooub  45563  limcresioolb  45564  fourierdlem48  46075  fourierdlem49  46076  fourierdlem102  46129  fourierdlem114  46141  sge0resplit  46327  elpglem2  48804