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

Theorem ssralv 3514
Description: Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006.)
Assertion
Ref Expression
ssralv  |-  ( A 
C_  B  ->  ( A. x  e.  B  ph 
->  A. x  e.  A  ph ) )
Distinct variable groups:    x, A    x, B
Allowed substitution hint:    ph( x)

Proof of Theorem ssralv
StepHypRef Expression
1 ssel 3448 . . 3  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21imim1d 75 . 2  |-  ( A 
C_  B  ->  (
( x  e.  B  ->  ph )  ->  (
x  e.  A  ->  ph ) ) )
32ralimdv2 2895 1  |-  ( A 
C_  B  ->  ( A. x  e.  B  ph 
->  A. x  e.  A  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   A.wral 2795    C_ wss 3426
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-ral 2800  df-in 3433  df-ss 3440
This theorem is referenced by:  iinss1  4281  disjiun  4380  poss  4741  sess2  4787  isores3  6125  isoini2  6129  smores  6913  smores2  6915  tfrlem5  6939  resixp  7398  ac6sfi  7657  iunfi  7700  ixpfi2  7710  dffi3  7782  marypha1lem  7784  ordtypelem2  7834  tcrank  8192  acndom  8322  pwsdompw  8474  ssfin3ds  8600  fin1a2s  8684  hsmexlem4  8699  domtriomlem  8712  zornn0g  8775  fpwwe2lem13  8910  ingru  9083  cshw1  12558  rexanuz  12935  cau3lem  12944  caubnd  12948  limsupgord  13052  limsupval2  13060  rlimres  13138  lo1res  13139  o1of2  13192  o1rlimmul  13198  isercolllem1  13244  climsup  13249  fsumiun  13386  pcfac  14063  vdwnnlem2  14159  firest  14473  imasaddfnlem  14568  imasvscafn  14577  psss  15486  tsrss  15495  cntz2ss  15952  cntzmhm2  15959  subgpgp  16200  efgsres  16339  dprdss  16631  ocv2ss  18207  mretopd  18812  tgcn  18972  tgcnp  18973  subbascn  18974  cnss2  18997  cncnp  19000  sslm  19019  t1ficld  19047  tgcmp  19120  1stcfb  19165  islly2  19204  dislly  19217  ptbasfi  19270  ptcnplem  19310  tx1stc  19339  qtoptop2  19388  fbunfip  19558  flftg  19685  txflf  19695  fclsbas  19710  fclsss1  19711  fclsss2  19712  alexsubb  19734  tmdgsum2  19783  metrest  20215  rescncf  20589  cnllycmp  20644  bndth  20646  fgcfil  20898  cfilres  20923  ivthlem2  21052  ivthlem3  21053  ovolsslem  21083  ovolfiniun  21100  finiunmbl  21141  volfiniun  21144  iunmbl  21150  ioombl1lem4  21158  dyadmax  21194  vitali  21209  mbfimaopnlem  21249  mbflimsup  21260  mbfi1flim  21317  ditgeq3  21441  dvferm  21576  rollelem  21577  dvivthlem1  21596  itgsubstlem  21636  aalioulem2  21915  ulmcaulem  21975  ulmss  21978  xrlimcnp  22478  lgsdchr  22803  pntlem3  22974  pntlemp  22975  pntleml  22976  nbgraf1olem1  23485  redwlk  23640  occon  24825  xrge0infss  26187  resspos  26254  resstos  26255  submarchi  26337  sigaclci  26709  measiun  26766  elmbfmvol2  26816  sibfof  26860  subfacp1lem3  27204  iccllyscon  27273  untint  27497  untangtr  27499  dfon2lem6  27735  dfon2lem8  27737  dfon2lem9  27738  setlikess  27790  poseq  27848  soseq  27849  finixpnum  28552  heicant  28564  volsupnfl  28574  comppfsc  28717  neibastop1  28718  neibastop2lem  28719  neibastop3  28721  prdstotbnd  28831  heibor1lem  28846  ispridl2  28976  elrfirn2  29170  rabdiophlem1  29277  dford3lem1  29513  kelac1  29554  acsfn1p  29694  climinf  29917  usg2wlkeq  30427  wwlknred  30493  wwlkm1edg  30505  clwlkisclwwlklem1  30587  clwwlkf  30594  wwlksubclwwlk  30604  extwwlkfablem2  30809  telescfzgsum  30951  telescgsum  30955  ssralv2  31536  ssralv2VD  31902  bnj1118  32275
  Copyright terms: Public domain W3C validator