MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  unexg Structured version   Visualization version   GIF version

Theorem unexg 7608
Description: A union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Sep-2006.)
Assertion
Ref Expression
unexg ((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)

Proof of Theorem unexg
StepHypRef Expression
1 elex 3451 . 2 (𝐴𝑉𝐴 ∈ V)
2 elex 3451 . 2 (𝐵𝑊𝐵 ∈ V)
3 unexb 7607 . . 3 ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴𝐵) ∈ V)
43biimpi 215 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐵) ∈ V)
51, 2, 4syl2an 596 1 ((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2107  Vcvv 3433  cun 3886
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353  ax-un 7597
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-sn 4563  df-pr 4565  df-uni 4841
This theorem is referenced by:  xpexg  7609  unexd  7613  difex2  7619  difsnexi  7620  eldifpw  7627  pwuncl  7629  ordunpr  7682  soex  7777  fnse  7983  suppun  8009  tposexg  8065  frrlem13  8123  wfrlem15OLD  8163  tfrlem12  8229  tfrlem16  8233  elmapresaun  8677  ralxpmap  8693  undifixp  8731  undom  8855  undomOLD  8856  domunsncan  8868  domssex2  8933  domssex  8934  mapunen  8942  sbthfilem  8993  fsuppunbi  9158  elfiun  9198  brwdom2  9341  unwdomg  9352  djuex  9675  djuexALT  9689  alephprc  9864  djudoml  9949  infunabs  9972  fin23lem11  10082  axdc2lem  10213  ttukeylem1  10274  fpwwe2lem12  10407  wunex2  10503  wuncval2  10512  hashunx  14110  hashf1lem1  14177  hashf1lem1OLD  14178  trclexlem  14714  trclun  14734  relexp0g  14742  relexpsucnnr  14745  isstruct2  16859  setsvalg  16876  setsid  16918  yonffth  18011  pwmndgplus  18583  dmdprdsplit2  19658  basdif0  22112  fiuncmp  22564  refun0  22675  ptbasfi  22741  dfac14lem  22777  ptrescn  22799  xkoptsub  22814  filconn  23043  isufil2  23068  ufileu  23079  filufint  23080  fmfnfmlem4  23117  fmfnfm  23118  fclsfnflim  23187  flimfnfcls  23188  ptcmplem1  23212  elply2  25366  plyss  25369  wlkp1lem4  28053  resf1o  31074  tocycfv  31385  tocycf  31393  locfinref  31800  esumsplit  32030  esumpad2  32033  sseqval  32364  bnj1149  32781  satfvsuc  33332  satf0suclem  33346  sat1el2xp  33350  fmlasuc0  33355  noeta2  33988  etasslt2  34017  scutbdaybnd2lim  34020  altxpexg  34289  hfun  34489  refssfne  34556  topjoin  34563  bj-2uplex  35221  ptrest  35785  poimirlem3  35789  paddval  37819  elrfi  40523  rclexi  41230  rtrclexlem  41231  trclubgNEW  41233  clcnvlem  41238  cnvrcl0  41240  dfrtrcl5  41244  iunrelexp0  41317  relexpmulg  41325  relexp01min  41328  relexpxpmin  41332  brtrclfv2  41342  sge0resplit  43951  sge0split  43954  setsv  44841  setrec1lem4  46407
  Copyright terms: Public domain W3C validator