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

Theorem unexg 6582
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 3102 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 elex 3102 . 2  |-  ( B  e.  W  ->  B  e.  _V )
3 unexb 6581 . . 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 1802   _Vcvv 3093    u. cun 3456
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pr 4672  ax-un 6573
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-rex 2797  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-sn 4011  df-pr 4013  df-uni 4231
This theorem is referenced by:  xpexg  6583  difex2  6588  difsnexi  6589  eldifpw  6593  ordunpr  6642  soex  6724  fnse  6898  suppun  6918  tposexg  6967  tfrlem12  7056  tfrlem16  7060  ralxpmap  7466  undifixp  7503  undom  7603  domunsncan  7615  domssex2  7675  domssex  7676  mapunen  7684  fsuppunbi  7848  elfiun  7888  brwdom2  7997  unwdomg  8008  alephprc  8478  cdadom3  8566  infunabs  8585  fin23lem11  8695  axdc2lem  8826  ttukeylem1  8887  fpwwe2lem13  9018  wunex2  9114  wuncval2  9123  hashunx  12428  hashf1lem1  12478  isstruct2  14513  setsvalg  14527  setsid  14545  yonffth  15422  dmdprdsplit2  16963  basdif0  19321  fiuncmp  19770  refun0  19882  ptbasfi  19948  dfac14lem  19984  ptrescn  20006  xkoptsub  20021  filcon  20250  isufil2  20275  ufileu  20286  filufint  20287  fmfnfmlem4  20324  fmfnfm  20325  fclsfnflim  20394  flimfnfcls  20395  ptcmplem1  20418  elply2  22459  plyss  22462  uhgraun  24176  umgraun  24193  vdgrun  24766  resf1o  27418  locfinref  27710  esumsplit  27929  sseqval  28193  wfrlem15  29325  nofulllem4  29433  altxpexg  29596  hfun  29803  ptrest  30016  refssfne  30144  topjoin  30151  elrfi  30594  elmapresaun  30672  uhgun  32214  bnj1149  33558  bj-2uplex  34292  paddval  35224
  Copyright terms: Public domain W3C validator