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

Theorem unexg 4521
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 2796 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 elex 2796 . 2  |-  ( B  e.  W  ->  B  e.  _V )
3 unexb 4520 . . 3  |-  ( ( A  e.  _V  /\  B  e.  _V )  <->  ( A  u.  B )  e.  _V )
43biimpi 186 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A  u.  B
)  e.  _V )
51, 2, 4syl2an 463 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  u.  B
)  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1684   _Vcvv 2788    u. cun 3150
This theorem is referenced by:  difex2  4525  eldifpw  4566  ordunpr  4617  xpexg  4800  soex  5122  fnse  6232  tposexg  6248  tfrlem12  6405  tfrlem16  6409  undifixp  6852  undom  6950  domunsncan  6962  domssex2  7021  domssex  7022  mapunen  7030  elfiun  7183  brwdom2  7287  unwdomg  7298  alephprc  7726  cdadom3  7814  infunabs  7833  fin23lem11  7943  axdc2lem  8074  ttukeylem1  8136  fpwwe2lem13  8264  wunex2  8360  wuncval2  8369  hashf1lem1  11393  isstruct2  13157  setsvalg  13171  setsid  13187  yonffth  14058  dmdprdsplit2  15281  basdif0  16691  tgdif0  16730  fiuncmp  17131  ptbasfi  17276  dfac14lem  17311  ptrescn  17333  xkoptsub  17348  filcon  17578  isufil2  17603  ufileu  17614  filufint  17615  fmfnfmlem4  17652  fmfnfm  17653  fclsfnflim  17722  flimfnfcls  17723  ptcmplem1  17746  elply2  19578  plyss  19581  esumsplit  23431  umgraun  23879  wfrlem15  24270  nofulllem4  24359  altxpexg  24512  hfun  24808  isconc2  26007  refssfne  26294  topjoin  26314  ralxpmap  26761  elrfi  26769  elmapresaun  26850  fnchoice  27700  uslgraun  28120  bnj1149  28824  paddval  29987
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-rex 2549  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-sn 3646  df-pr 3647  df-uni 3828
  Copyright terms: Public domain W3C validator