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 2798 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 elex 2798 . 2  |-  ( B  e.  W  ->  B  e.  _V )
3 unexb 4520 . . 3  |-  ( ( A  e.  _V  /\  B  e.  _V )  <->  ( A  u.  B )  e.  _V )
43biimpi 188 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A  u.  B
)  e.  _V )
51, 2, 4syl2an 465 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  u.  B
)  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1685   _Vcvv 2790    u. cun 3152
This theorem is referenced by:  difex2  4525  eldifpw  4566  ordunpr  4617  xpexg  4800  soex  5122  fnse  6194  tposexg  6210  tfrlem12  6401  tfrlem16  6405  undifixp  6848  undom  6946  domunsncan  6958  domssex2  7017  domssex  7018  mapunen  7026  elfiun  7179  brwdom2  7283  unwdomg  7294  alephprc  7722  cdadom3  7810  infunabs  7829  fin23lem11  7939  axdc2lem  8070  ttukeylem1  8132  fpwwe2lem13  8260  wunex2  8356  wuncval2  8365  hashf1lem1  11388  isstruct2  13152  setsvalg  13166  setsid  13182  yonffth  14053  dmdprdsplit2  15276  basdif0  16686  tgdif0  16725  fiuncmp  17126  ptbasfi  17271  dfac14lem  17306  ptrescn  17328  xkoptsub  17343  filcon  17573  isufil2  17598  ufileu  17609  filufint  17610  fmfnfmlem4  17647  fmfnfm  17648  fclsfnflim  17717  flimfnfcls  17718  ptcmplem1  17741  elply2  19573  plyss  19576  umgraun  23284  wfrlem15  23672  axfelem14  23761  altxpexg  23920  hfun  24216  isconc2  25407  refssfne  25694  topjoin  25714  ralxpmap  26161  elrfi  26169  elmapresaun  26250  fnchoice  27100  bnj1149  28092  paddval  29255
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-rex 2551  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-sn 3648  df-pr 3649  df-uni 3830
  Copyright terms: Public domain W3C validator