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

Theorem ssralv 3505
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 3438 . . 3  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21imim1d 78 . 2  |-  ( A 
C_  B  ->  (
( x  e.  B  ->  ph )  ->  (
x  e.  A  ->  ph ) ) )
32ralimdv2 2807 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 1898   A.wral 2749    C_ wss 3416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-ral 2754  df-in 3423  df-ss 3430
This theorem is referenced by:  intss  4269  iinss1  4305  disjiun  4409  poss  4779  sess2  4825  isores3  6256  isoini2  6260  smores  7102  smores2  7104  tfrlem5  7129  resixp  7588  ac6sfi  7846  iunfi  7893  ixpfi2  7903  dffi3  7976  marypha1lem  7978  ordtypelem2  8065  tcrank  8386  acndom  8513  pwsdompw  8665  ssfin3ds  8791  fin1a2s  8875  hsmexlem4  8890  domtriomlem  8903  zornn0g  8966  fpwwe2lem13  9098  ingru  9271  cshw1  12964  rexanuz  13463  cau3lem  13472  caubnd  13476  limsupgord  13583  limsupval2  13595  limsupval2OLD  13596  rlimres  13677  lo1res  13678  o1of2  13731  o1rlimmul  13737  isercolllem1  13783  climsup  13788  fsumiun  13936  lcmfunsnlem1  14665  coprmprod  14733  pcfac  14899  vdwnnlem2  15001  firest  15386  imasaddfnlem  15489  imasvscafn  15498  psss  16515  tsrss  16524  cntz2ss  17041  cntzmhm2  17048  subgpgp  17304  efgsres  17443  telgsumfzs  17674  telgsums  17678  dprdss  17717  ocv2ss  19291  mretopd  20163  tgcn  20323  tgcnp  20324  subbascn  20325  cnss2  20348  cncnp  20351  sslm  20370  t1ficld  20398  tgcmp  20471  1stcfb  20515  islly2  20554  dislly  20567  comppfsc  20602  ptbasfi  20651  ptcnplem  20691  tx1stc  20720  qtoptop2  20769  fbunfip  20939  flftg  21066  txflf  21076  fclsbas  21091  fclsss1  21092  fclsss2  21093  alexsubb  21116  tmdgsum2  21166  metrest  21594  rescncf  21984  cnllycmp  22039  bndth  22041  fgcfil  22296  cfilres  22321  ivthlem2  22458  ivthlem3  22459  ovolsslem  22492  ovolfiniun  22509  finiunmbl  22553  volfiniun  22556  iunmbl  22562  ioombl1lem4  22570  dyadmax  22612  vitali  22627  mbfimaopnlem  22667  mbflimsup  22679  mbflimsupOLD  22680  mbfi1flim  22737  ditgeq3  22861  dvferm  22996  rollelem  22997  dvivthlem1  23016  itgsubstlem  23056  aalioulem2  23345  ulmcaulem  23405  ulmss  23408  xrlimcnp  23950  lgsdchr  24332  pntlem3  24503  pntlemp  24504  pntleml  24505  nbgraf1olem1  25225  redwlk  25392  usg2wlkeq  25492  wwlknred  25507  wwlkm1edg  25519  clwlkisclwwlklem1  25571  clwwlkf  25578  wwlksubclwwlk  25588  extwwlkfablem2  25862  occon  26996  xrge0infss  28392  xrge0infssOLD  28393  resspos  28472  resstos  28473  submarchi  28554  sigaclci  29005  measiun  29091  elmbfmvol2  29139  sibfof  29223  bnj1118  29843  subfacp1lem3  29955  iccllyscon  30023  untint  30389  untangtr  30391  dfon2lem6  30484  dfon2lem8  30486  dfon2lem9  30487  poseq  30541  soseq  30542  nosepon  30606  neibastop1  31065  neibastop2lem  31066  neibastop3  31068  finixpnum  31976  ptrecube  31986  poimirlem26  32012  poimirlem27  32013  poimirlem30  32016  heicant  32021  volsupnfl  32031  prdstotbnd  32172  heibor1lem  32187  ispridl2  32317  elrfirn2  35584  rabdiophlem1  35690  dford3lem1  35927  kelac1  35967  acsfn1p  36111  ssralv2  36933  ssralv2VD  37304  climinf  37770  climinfOLD  37771  iccpartres  38867  red1wlk  39813
  Copyright terms: Public domain W3C validator