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

Theorem unexg 6379
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  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  u.  B
)  e.  _V )

Proof of Theorem unexg
StepHypRef Expression
1 elex 2979 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 elex 2979 . 2  |-  ( B  e.  W  ->  B  e.  _V )
3 unexb 6378 . . 3  |-  ( ( A  e.  _V  /\  B  e.  _V )  <->  ( A  u.  B )  e.  _V )
43biimpi 194 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A  u.  B
)  e.  _V )
51, 2, 4syl2an 477 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  u.  B
)  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1756   _Vcvv 2970    u. cun 3324
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422  ax-sep 4411  ax-nul 4419  ax-pr 4529  ax-un 6370
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-rex 2719  df-v 2972  df-dif 3329  df-un 3331  df-in 3333  df-ss 3340  df-nul 3636  df-sn 3876  df-pr 3878  df-uni 4090
This theorem is referenced by:  difex2  6381  difsnexi  6382  eldifpw  6386  ordunpr  6435  xpexg  6505  soex  6519  fnse  6687  suppun  6707  tposexg  6757  tfrlem12  6846  tfrlem16  6850  ralxpmap  7260  undifixp  7297  undom  7397  domunsncan  7409  domssex2  7469  domssex  7470  mapunen  7478  fsuppunbi  7639  elfiun  7678  brwdom2  7786  unwdomg  7797  alephprc  8267  cdadom3  8355  infunabs  8374  fin23lem11  8484  axdc2lem  8615  ttukeylem1  8676  fpwwe2lem13  8807  wunex2  8903  wuncval2  8912  hashunx  12147  hashf1lem1  12206  isstruct2  14181  setsvalg  14195  setsid  14213  yonffth  15092  dmdprdsplit2  16543  basdif0  18556  tgdif0  18595  fiuncmp  19005  ptbasfi  19152  dfac14lem  19188  ptrescn  19210  xkoptsub  19225  filcon  19454  isufil2  19479  ufileu  19490  filufint  19491  fmfnfmlem4  19528  fmfnfm  19529  fclsfnflim  19598  flimfnfcls  19599  ptcmplem1  19622  elply2  21662  plyss  21665  uhgraun  23243  umgraun  23260  vdgrun  23569  resf1o  26028  esumsplit  26504  sseqval  26769  wfrlem15  27736  nofulllem4  27844  altxpexg  28007  hfun  28214  ptrest  28422  refssfne  28563  topjoin  28583  elrfi  29027  elmapresaun  29106  bnj1149  31783  bj-2uplex  32512  paddval  33439
  Copyright terms: Public domain W3C validator