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

Theorem unexg 6606
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 3089 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 elex 3089 . 2  |-  ( B  e.  W  ->  B  e.  _V )
3 unexb 6605 . . 3  |-  ( ( A  e.  _V  /\  B  e.  _V )  <->  ( A  u.  B )  e.  _V )
43biimpi 197 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A  u.  B
)  e.  _V )
51, 2, 4syl2an 479 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  u.  B
)  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    e. wcel 1872   _Vcvv 3080    u. cun 3434
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660  ax-un 6597
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-rex 2777  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-sn 3999  df-pr 4001  df-uni 4220
This theorem is referenced by:  xpexg  6607  difex2  6612  difsnexi  6613  eldifpw  6617  ordunpr  6667  soex  6750  fnse  6924  suppun  6946  tposexg  6998  wfrlem15  7061  tfrlem12  7118  tfrlem16  7122  ralxpmap  7532  undifixp  7569  undom  7669  domunsncan  7681  domssex2  7741  domssex  7742  mapunen  7750  fsuppunbi  7913  elfiun  7953  brwdom2  8097  unwdomg  8108  alephprc  8537  cdadom3  8625  infunabs  8644  fin23lem11  8754  axdc2lem  8885  ttukeylem1  8946  fpwwe2lem13  9074  wunex2  9170  wuncval2  9179  hashunx  12571  hashf1lem1  12622  trclexlem  13058  trclun  13078  relexp0g  13085  relexpsucnnr  13088  isstruct2  15129  setsvalg  15144  setsid  15163  yonffth  16168  dmdprdsplit2  17678  basdif0  19966  fiuncmp  20417  refun0  20528  ptbasfi  20594  dfac14lem  20630  ptrescn  20652  xkoptsub  20667  filcon  20896  isufil2  20921  ufileu  20932  filufint  20933  fmfnfmlem4  20970  fmfnfm  20971  fclsfnflim  21040  flimfnfcls  21041  ptcmplem1  21065  elply2  23148  plyss  23151  uhgraun  25036  umgraun  25053  vdgrun  25627  resf1o  28321  locfinref  28676  esumsplit  28882  esumpad2  28885  sseqval  29229  bnj1149  29612  nofulllem4  30599  altxpexg  30750  hfun  30950  refssfne  31019  topjoin  31026  bj-2uplex  31584  ptrest  31903  poimirlem3  31907  paddval  33332  elrfi  35505  elmapresaun  35582  rclexi  36192  rtrclexlem  36193  trclubgNEW  36195  clcnvlem  36200  cnvrcl0  36202  dfrtrcl5  36206  iunrelexp0  36264  relexpmulg  36272  relexp01min  36275  relexpxpmin  36279  brtrclfv2  36289  sge0resplit  38156  sge0split  38159  uhgun  39312
  Copyright terms: Public domain W3C validator