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

Theorem ssralv 3557
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 3491 . . 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 2864 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 1762   A.wral 2807    C_ wss 3469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-ral 2812  df-in 3476  df-ss 3483
This theorem is referenced by:  iinss1  4331  disjiun  4430  poss  4795  sess2  4841  isores3  6210  isoini2  6214  smores  7013  smores2  7015  tfrlem5  7039  resixp  7494  ac6sfi  7753  iunfi  7797  ixpfi2  7807  dffi3  7880  marypha1lem  7882  ordtypelem2  7933  tcrank  8291  acndom  8421  pwsdompw  8573  ssfin3ds  8699  fin1a2s  8783  hsmexlem4  8798  domtriomlem  8811  zornn0g  8874  fpwwe2lem13  9009  ingru  9182  cshw1  12740  rexanuz  13127  cau3lem  13136  caubnd  13140  limsupgord  13244  limsupval2  13252  rlimres  13330  lo1res  13331  o1of2  13384  o1rlimmul  13390  isercolllem1  13436  climsup  13441  fsumiun  13584  pcfac  14266  vdwnnlem2  14362  firest  14677  imasaddfnlem  14772  imasvscafn  14781  psss  15690  tsrss  15699  cntz2ss  16158  cntzmhm2  16165  subgpgp  16406  efgsres  16545  telgsumfzs  16802  telgsums  16806  dprdss  16859  ocv2ss  18464  mretopd  19352  tgcn  19512  tgcnp  19513  subbascn  19514  cnss2  19537  cncnp  19540  sslm  19559  t1ficld  19587  tgcmp  19660  1stcfb  19705  islly2  19744  dislly  19757  ptbasfi  19810  ptcnplem  19850  tx1stc  19879  qtoptop2  19928  fbunfip  20098  flftg  20225  txflf  20235  fclsbas  20250  fclsss1  20251  fclsss2  20252  alexsubb  20274  tmdgsum2  20323  metrest  20755  rescncf  21129  cnllycmp  21184  bndth  21186  fgcfil  21438  cfilres  21463  ivthlem2  21592  ivthlem3  21593  ovolsslem  21623  ovolfiniun  21640  finiunmbl  21682  volfiniun  21685  iunmbl  21691  ioombl1lem4  21699  dyadmax  21735  vitali  21750  mbfimaopnlem  21790  mbflimsup  21801  mbfi1flim  21858  ditgeq3  21982  dvferm  22117  rollelem  22118  dvivthlem1  22137  itgsubstlem  22177  aalioulem2  22456  ulmcaulem  22516  ulmss  22519  xrlimcnp  23019  lgsdchr  23344  pntlem3  23515  pntlemp  23516  pntleml  23517  nbgraf1olem1  24103  redwlk  24270  usg2wlkeq  24370  wwlknred  24385  wwlkm1edg  24397  clwlkisclwwlklem1  24449  clwwlkf  24456  wwlksubclwwlk  24466  occon  25731  xrge0infss  27098  resspos  27159  resstos  27160  submarchi  27242  sigaclci  27622  measiun  27679  elmbfmvol2  27728  sibfof  27772  subfacp1lem3  28116  iccllyscon  28185  untint  28409  untangtr  28411  dfon2lem6  28647  dfon2lem8  28649  dfon2lem9  28650  setlikess  28702  poseq  28760  soseq  28761  finixpnum  29465  heicant  29477  volsupnfl  29487  comppfsc  29630  neibastop1  29631  neibastop2lem  29632  neibastop3  29634  prdstotbnd  29744  heibor1lem  29759  ispridl2  29889  elrfirn2  30083  rabdiophlem1  30189  dford3lem1  30425  kelac1  30466  acsfn1p  30606  climinf  30967  extwwlkfablem2  31797  ssralv2  32255  ssralv2VD  32621  bnj1118  32994
  Copyright terms: Public domain W3C validator