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

Theorem unexg 6576
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 3115 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 elex 3115 . 2  |-  ( B  e.  W  ->  B  e.  _V )
3 unexb 6575 . . 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 1762   _Vcvv 3106    u. cun 3467
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679  ax-un 6567
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-rex 2813  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-sn 4021  df-pr 4023  df-uni 4239
This theorem is referenced by:  difex2  6578  difsnexi  6579  eldifpw  6583  ordunpr  6632  xpexg  6702  soex  6717  fnse  6890  suppun  6910  tposexg  6959  tfrlem12  7048  tfrlem16  7052  ralxpmap  7458  undifixp  7495  undom  7595  domunsncan  7607  domssex2  7667  domssex  7668  mapunen  7676  fsuppunbi  7839  elfiun  7879  brwdom2  7988  unwdomg  7999  alephprc  8469  cdadom3  8557  infunabs  8576  fin23lem11  8686  axdc2lem  8817  ttukeylem1  8878  fpwwe2lem13  9009  wunex2  9105  wuncval2  9114  hashunx  12409  hashf1lem1  12457  isstruct2  14488  setsvalg  14502  setsid  14520  yonffth  15400  dmdprdsplit2  16878  basdif0  19214  tgdif0  19253  fiuncmp  19663  ptbasfi  19810  dfac14lem  19846  ptrescn  19868  xkoptsub  19883  filcon  20112  isufil2  20137  ufileu  20148  filufint  20149  fmfnfmlem4  20186  fmfnfm  20187  fclsfnflim  20256  flimfnfcls  20257  ptcmplem1  20280  elply2  22321  plyss  22324  uhgraun  23974  umgraun  23991  vdgrun  24563  resf1o  27211  esumsplit  27689  sseqval  27953  wfrlem15  28920  nofulllem4  29028  altxpexg  29191  hfun  29398  ptrest  29612  refssfne  29753  topjoin  29773  elrfi  30217  elmapresaun  30295  bnj1149  32805  bj-2uplex  33536  paddval  34469
  Copyright terms: Public domain W3C validator