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

Theorem unexg 4701
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 2956 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 elex 2956 . 2  |-  ( B  e.  W  ->  B  e.  _V )
3 unexb 4700 . . 3  |-  ( ( A  e.  _V  /\  B  e.  _V )  <->  ( A  u.  B )  e.  _V )
43biimpi 187 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A  u.  B
)  e.  _V )
51, 2, 4syl2an 464 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  u.  B
)  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725   _Vcvv 2948    u. cun 3310
This theorem is referenced by:  difex2  4705  eldifpw  4746  ordunpr  4797  xpexg  4980  soex  5310  fnse  6454  tposexg  6484  tfrlem12  6641  tfrlem16  6645  undifixp  7089  undom  7187  domunsncan  7199  domssex2  7258  domssex  7259  mapunen  7267  elfiun  7426  brwdom2  7530  unwdomg  7541  alephprc  7969  cdadom3  8057  infunabs  8076  fin23lem11  8186  axdc2lem  8317  ttukeylem1  8378  fpwwe2lem13  8506  wunex2  8602  wuncval2  8611  hashunx  11648  hashf1lem1  11692  isstruct2  13466  setsvalg  13480  setsid  13496  yonffth  14369  dmdprdsplit2  15592  basdif0  17006  tgdif0  17045  fiuncmp  17455  ptbasfi  17601  dfac14lem  17637  ptrescn  17659  xkoptsub  17674  filcon  17903  isufil2  17928  ufileu  17939  filufint  17940  fmfnfmlem4  17977  fmfnfm  17978  fclsfnflim  18047  flimfnfcls  18048  ptcmplem1  18071  elply2  20103  plyss  20106  uhgraun  21334  umgraun  21351  vdgrun  21660  esumsplit  24435  wfrlem15  25525  nofulllem4  25614  altxpexg  25771  hfun  26067  refssfne  26311  topjoin  26331  ralxpmap  26679  elrfi  26685  elmapresaun  26766  bnj1149  29017  paddval  30434
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395  ax-un 4692
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-rex 2703  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-sn 3812  df-pr 3813  df-uni 4008
  Copyright terms: Public domain W3C validator