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

Theorem unexg 4479
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 2765 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 elex 2765 . 2  |-  ( B  e.  W  ->  B  e.  _V )
3 unexb 4478 . . 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 1621   _Vcvv 2757    u. cun 3111
This theorem is referenced by:  difex2  4483  eldifpw  4524  ordunpr  4575  xpexg  4774  soex  5096  fnse  6152  tposexg  6168  tfrlem12  6359  tfrlem16  6363  undifixp  6806  undom  6904  domunsncan  6916  domssex2  6975  domssex  6976  mapunen  6984  elfiun  7137  brwdom2  7241  unwdomg  7252  alephprc  7680  cdadom3  7768  infunabs  7787  fin23lem11  7897  axdc2lem  8028  ttukeylem1  8090  fpwwe2lem13  8218  wunex2  8314  wuncval2  8323  hashf1lem1  11344  isstruct2  13105  setsvalg  13119  setsid  13135  yonffth  14006  dmdprdsplit2  15229  basdif0  16639  tgdif0  16678  fiuncmp  17079  ptbasfi  17224  dfac14lem  17259  ptrescn  17281  xkoptsub  17296  filcon  17526  isufil2  17551  ufileu  17562  filufint  17563  fmfnfmlem4  17600  fmfnfm  17601  fclsfnflim  17670  flimfnfcls  17671  ptcmplem1  17694  elply2  19526  plyss  19529  umgraun  23237  wfrlem15  23625  axfelem14  23714  altxpexg  23873  hfun  24169  isconc2  25360  refssfne  25647  topjoin  25667  ralxpmap  26114  elrfi  26122  elmapresaun  26203  fnchoice  27054  bnj1149  27857  paddval  29138
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4101  ax-nul 4109  ax-pr 4172  ax-un 4470
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-rex 2522  df-v 2759  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-nul 3417  df-sn 3606  df-pr 3607  df-uni 3788
  Copyright terms: Public domain W3C validator