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

Theorem uniss 3864
Description: Subclass relationship for class union. Theorem 61 of [Suppes] p. 39. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
Assertion
Ref Expression
uniss  |-  ( A 
C_  B  ->  U. A  C_ 
U. B )

Proof of Theorem uniss
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssel 3187 . . . . 5  |-  ( A 
C_  B  ->  (
y  e.  A  -> 
y  e.  B ) )
21anim2d 548 . . . 4  |-  ( A 
C_  B  ->  (
( x  e.  y  /\  y  e.  A
)  ->  ( x  e.  y  /\  y  e.  B ) ) )
32eximdv 1612 . . 3  |-  ( A 
C_  B  ->  ( E. y ( x  e.  y  /\  y  e.  A )  ->  E. y
( x  e.  y  /\  y  e.  B
) ) )
4 eluni 3846 . . 3  |-  ( x  e.  U. A  <->  E. y
( x  e.  y  /\  y  e.  A
) )
5 eluni 3846 . . 3  |-  ( x  e.  U. B  <->  E. y
( x  e.  y  /\  y  e.  B
) )
63, 4, 53imtr4g 261 . 2  |-  ( A 
C_  B  ->  (
x  e.  U. A  ->  x  e.  U. B
) )
76ssrdv 3198 1  |-  ( A 
C_  B  ->  U. A  C_ 
U. B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   E.wex 1531    e. wcel 1696    C_ wss 3165   U.cuni 3843
This theorem is referenced by:  unissi  3866  unissd  3867  unidif  3875  intssuni2  3903  uniintsn  3915  unixpss  4815  relfld  5214  dffv2  5608  riotassuni  6359  onfununi  6374  unifpw  7174  fiuni  7197  trcl  7426  rankuni  7551  dfac2a  7772  cflm  7892  coflim  7903  cfslbn  7909  fin23lem29  7983  fin23lem30  7984  fin23lem41  7994  fin1a2lem12  8053  tskuni  8421  prdsval  13371  prdsbas  13373  prdsplusg  13374  prdsmulr  13375  prdsvsca  13376  prdsds  13379  prdshom  13382  mrcssv  13532  isacs1i  13575  catcfuccl  13957  catcxpccl  13997  isacs3lem  14285  mrelatlub  14305  mreclat  14306  psss  14339  dprdres  15279  dprd2da  15293  dmdprdsplit2lem  15296  tgval2  16710  eltg4i  16714  eltg3i  16715  unitg  16721  tgss  16722  tgcl  16723  distop  16749  fctop  16757  cctop  16759  ntrss2  16810  isopn3  16819  mretopd  16845  ordtbas  16938  cmpcov2  17133  tgcmp  17144  cmpcld  17145  uncmp  17146  cmpfi  17151  kgentopon  17249  txcmplem2  17352  filcon  17594  alexsublem  17754  alexsubALTlem3  17759  alexsubALTlem4  17760  alexsubALT  17761  ptcmplem3  17764  cldsubg  17809  bndth  18472  uniioombllem3  18956  uniioombllem4  18957  uniioombllem5  18958  dyadmbllem  18970  shsupcl  21933  hsupss  21936  shsupunss  21941  shatomistici  22957  cvmscld  23819  cvmliftlem15  23844  frrlem5c  24358  nofulllem3  24429  onsucsuccmpi  24954  uuniin  25190  inttrp  25211  inposet  25381  intfmu2  25622  bwt2  25695  tartarmap  25991  fnessref  26396  comppfsc  26410  fnemeet1  26418  fnejoin1  26420  filnetlem3  26432  cover2  26461  heibor1  26637  heiborlem1  26638  heiborlem10  26647  hbt  27437  lssats  29824  lpssat  29825  lssatle  29827  lssat  29828  dicval  31988
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179  df-uni 3844
  Copyright terms: Public domain W3C validator