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

Theorem uniss 3848
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 3174 . . . . 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 1608 . . 3  |-  ( A 
C_  B  ->  ( E. y ( x  e.  y  /\  y  e.  A )  ->  E. y
( x  e.  y  /\  y  e.  B
) ) )
4 eluni 3830 . . 3  |-  ( x  e.  U. A  <->  E. y
( x  e.  y  /\  y  e.  A
) )
5 eluni 3830 . . 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 3185 1  |-  ( A 
C_  B  ->  U. A  C_ 
U. B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   E.wex 1528    e. wcel 1684    C_ wss 3152   U.cuni 3827
This theorem is referenced by:  unissi  3850  unissd  3851  unidif  3859  intssuni2  3887  uniintsn  3899  unixpss  4799  relfld  5198  dffv2  5592  riotassuni  6343  onfununi  6358  unifpw  7158  fiuni  7181  trcl  7410  rankuni  7535  dfac2a  7756  cflm  7876  coflim  7887  cfslbn  7893  fin23lem29  7967  fin23lem30  7968  fin23lem41  7978  fin1a2lem12  8037  tskuni  8405  prdsval  13355  prdsbas  13357  prdsplusg  13358  prdsmulr  13359  prdsvsca  13360  prdsds  13363  prdshom  13366  mrcssv  13516  isacs1i  13559  catcfuccl  13941  catcxpccl  13981  isacs3lem  14269  mrelatlub  14289  mreclat  14290  psss  14323  dprdres  15263  dprd2da  15277  dmdprdsplit2lem  15280  tgval2  16694  eltg4i  16698  eltg3i  16699  unitg  16705  tgss  16706  tgcl  16707  distop  16733  fctop  16741  cctop  16743  ntrss2  16794  isopn3  16803  mretopd  16829  ordtbas  16922  cmpcov2  17117  tgcmp  17128  cmpcld  17129  uncmp  17130  cmpfi  17135  kgentopon  17233  txcmplem2  17336  filcon  17578  alexsublem  17738  alexsubALTlem3  17743  alexsubALTlem4  17744  alexsubALT  17745  ptcmplem3  17748  cldsubg  17793  bndth  18456  uniioombllem3  18940  uniioombllem4  18941  uniioombllem5  18942  dyadmbllem  18954  shsupcl  21917  hsupss  21920  shsupunss  21925  shatomistici  22941  cvmscld  23804  cvmliftlem15  23829  frrlem5c  24287  nofulllem3  24358  onsucsuccmpi  24882  uuniin  25087  inttrp  25108  inposet  25278  intfmu2  25519  bwt2  25592  tartarmap  25888  fnessref  26293  comppfsc  26307  fnemeet1  26315  fnejoin1  26317  filnetlem3  26329  cover2  26358  heibor1  26534  heiborlem1  26535  heiborlem10  26544  hbt  27334  lssats  29202  lpssat  29203  lssatle  29205  lssat  29206  dicval  31366
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166  df-uni 3828
  Copyright terms: Public domain W3C validator