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

Theorem unexg 6522
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 3060 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 elex 3060 . 2  |-  ( B  e.  W  ->  B  e.  _V )
3 unexb 6521 . . 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 475 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  u.  B
)  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1836   _Vcvv 3051    u. cun 3404
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374  ax-sep 4505  ax-nul 4513  ax-pr 4618  ax-un 6513
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-ne 2593  df-rex 2752  df-v 3053  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3729  df-sn 3962  df-pr 3964  df-uni 4181
This theorem is referenced by:  xpexg  6523  difex2  6528  difsnexi  6529  eldifpw  6533  ordunpr  6582  soex  6664  fnse  6838  suppun  6860  tposexg  6909  tfrlem12  6998  tfrlem16  7002  ralxpmap  7409  undifixp  7446  undom  7546  domunsncan  7558  domssex2  7618  domssex  7619  mapunen  7627  fsuppunbi  7787  elfiun  7827  brwdom2  7936  unwdomg  7947  alephprc  8415  cdadom3  8503  infunabs  8522  fin23lem11  8632  axdc2lem  8763  ttukeylem1  8824  fpwwe2lem13  8953  wunex2  9049  wuncval2  9058  hashunx  12380  hashf1lem1  12431  trclexlem  12855  trclun  12875  relexp0g  12882  relexpsucnnr  12885  isstruct2  14666  setsvalg  14681  setsid  14700  yonffth  15693  dmdprdsplit2  17231  basdif0  19562  fiuncmp  20013  refun0  20124  ptbasfi  20190  dfac14lem  20226  ptrescn  20248  xkoptsub  20263  filcon  20492  isufil2  20517  ufileu  20528  filufint  20529  fmfnfmlem4  20566  fmfnfm  20567  fclsfnflim  20636  flimfnfcls  20637  ptcmplem1  20660  elply2  22701  plyss  22704  uhgraun  24457  umgraun  24474  vdgrun  25047  resf1o  27737  locfinref  28033  esumsplit  28236  esumpad2  28239  sseqval  28550  wfrlem15  29562  nofulllem4  29670  altxpexg  29821  hfun  30028  ptrest  30253  refssfne  30382  topjoin  30389  elrfi  30832  elmapresaun  30909  uhgun  32737  bnj1149  34237  bj-2uplex  34967  paddval  35974  relexp01min  38276  iunrelexp0  38281  relexpxpmin  38283  relexpmulg  38285  brtrclfv2  38297
  Copyright terms: Public domain W3C validator