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

Theorem uniss 3849
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 )
Dummy variables  x  y are mutually distinct and distinct from all other variables.

Proof of Theorem uniss
StepHypRef Expression
1 ssel 3175 . . . . 5  |-  ( A 
C_  B  ->  (
y  e.  A  -> 
y  e.  B ) )
21anim2d 550 . . . 4  |-  ( A 
C_  B  ->  (
( x  e.  y  /\  y  e.  A
)  ->  ( x  e.  y  /\  y  e.  B ) ) )
32eximdv 1609 . . 3  |-  ( A 
C_  B  ->  ( E. y ( x  e.  y  /\  y  e.  A )  ->  E. y
( x  e.  y  /\  y  e.  B
) ) )
4 eluni 3831 . . 3  |-  ( x  e.  U. A  <->  E. y
( x  e.  y  /\  y  e.  A
) )
5 eluni 3831 . . 3  |-  ( x  e.  U. B  <->  E. y
( x  e.  y  /\  y  e.  B
) )
63, 4, 53imtr4g 263 . 2  |-  ( A 
C_  B  ->  (
x  e.  U. A  ->  x  e.  U. B
) )
76ssrdv 3186 1  |-  ( A 
C_  B  ->  U. A  C_ 
U. B )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360   E.wex 1529    e. wcel 1685    C_ wss 3153   U.cuni 3828
This theorem is referenced by:  unissi  3851  unissd  3852  unidif  3860  intssuni2  3888  uniintsn  3900  unixpss  4798  relfld  5196  dffv2  5553  riotassuni  6338  onfununi  6353  unifpw  7153  fiuni  7176  trcl  7405  rankuni  7530  dfac2a  7751  cflm  7871  coflim  7882  cfslbn  7888  fin23lem29  7962  fin23lem30  7963  fin23lem41  7973  fin1a2lem12  8032  tskuni  8400  prdsval  13349  prdsbas  13351  prdsplusg  13352  prdsmulr  13353  prdsvsca  13354  prdsds  13357  prdshom  13360  mrcssv  13510  isacs1i  13553  catcfuccl  13935  catcxpccl  13975  isacs3lem  14263  mrelatlub  14283  mreclat  14284  psss  14317  dprdres  15257  dprd2da  15271  dmdprdsplit2lem  15274  tgval2  16688  eltg4i  16692  eltg3i  16693  unitg  16699  tgss  16700  tgcl  16701  distop  16727  fctop  16735  cctop  16737  ntrss2  16788  isopn3  16797  mretopd  16823  ordtbas  16916  cmpcov2  17111  tgcmp  17122  cmpcld  17123  uncmp  17124  cmpfi  17129  kgentopon  17227  txcmplem2  17330  filcon  17572  alexsublem  17732  alexsubALTlem3  17737  alexsubALTlem4  17738  alexsubALT  17739  ptcmplem3  17742  cldsubg  17787  bndth  18450  uniioombllem3  18934  uniioombllem4  18935  uniioombllem5  18936  dyadmbllem  18948  shsupcl  21909  hsupss  21912  shsupunss  21917  shatomistici  22933  cvmscld  23208  cvmliftlem15  23233  frrlem5c  23688  onsucsuccmpi  24289  uuniin  24485  inttrp  24506  inposet  24677  intfmu2  24918  bwt2  24991  tartarmap  25287  fnessref  25692  comppfsc  25706  fnemeet1  25714  fnejoin1  25716  filnetlem3  25728  cover2  25757  heibor1  25933  heiborlem1  25934  heiborlem10  25943  hbt  26733  lssats  28469  lpssat  28470  lssatle  28472  lssat  28473  dicval  30633
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160  df-ss 3167  df-uni 3829
  Copyright terms: Public domain W3C validator