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

Theorem ssralv 3404
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 3338 . . 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 2786 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 1755   A.wral 2705    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-ral 2710  df-in 3323  df-ss 3330
This theorem is referenced by:  iinss1  4171  disjiun  4270  poss  4630  sess2  4676  isores3  6013  isoini2  6017  smores  6799  smores2  6801  tfrlem5  6825  resixp  7286  ac6sfi  7544  iunfi  7587  ixpfi2  7597  dffi3  7669  marypha1lem  7671  ordtypelem2  7721  tcrank  8079  acndom  8209  pwsdompw  8361  ssfin3ds  8487  fin1a2s  8571  hsmexlem4  8586  domtriomlem  8599  zornn0g  8662  fpwwe2lem13  8797  ingru  8970  cshw1  12440  rexanuz  12817  cau3lem  12826  caubnd  12830  limsupgord  12934  limsupval2  12942  rlimres  13020  lo1res  13021  o1of2  13074  o1rlimmul  13080  isercolllem1  13126  climsup  13131  fsumiun  13267  pcfac  13944  vdwnnlem2  14040  firest  14354  imasaddfnlem  14449  imasvscafn  14458  psss  15367  tsrss  15376  cntz2ss  15830  cntzmhm2  15837  subgpgp  16076  efgsres  16215  dprdss  16500  ocv2ss  17940  mretopd  18538  tgcn  18698  tgcnp  18699  subbascn  18700  cnss2  18723  cncnp  18726  sslm  18745  t1ficld  18773  tgcmp  18846  1stcfb  18891  islly2  18930  dislly  18943  ptbasfi  18996  ptcnplem  19036  tx1stc  19065  qtoptop2  19114  fbunfip  19284  flftg  19411  txflf  19421  fclsbas  19436  fclsss1  19437  fclsss2  19438  alexsubb  19460  tmdgsum2  19509  metrest  19941  rescncf  20315  cnllycmp  20370  bndth  20372  fgcfil  20624  cfilres  20649  ivthlem2  20778  ivthlem3  20779  ovolsslem  20809  ovolfiniun  20826  finiunmbl  20867  volfiniun  20870  iunmbl  20876  ioombl1lem4  20884  dyadmax  20920  vitali  20935  mbfimaopnlem  20975  mbflimsup  20986  mbfi1flim  21043  ditgeq3  21167  dvferm  21302  rollelem  21303  dvivthlem1  21322  itgsubstlem  21362  aalioulem2  21684  ulmcaulem  21744  ulmss  21747  xrlimcnp  22247  lgsdchr  22572  pntlem3  22743  pntlemp  22744  pntleml  22745  nbgraf1olem1  23173  redwlk  23328  occon  24513  resspos  25943  resstos  25944  submarchi  26027  sigaclci  26429  measiun  26486  elmbfmvol2  26536  sibfof  26574  subfacp1lem3  26918  iccllyscon  26987  untint  27210  untangtr  27212  dfon2lem6  27448  dfon2lem8  27450  dfon2lem9  27451  setlikess  27503  poseq  27561  soseq  27562  finixpnum  28258  heicant  28270  volsupnfl  28280  comppfsc  28423  neibastop1  28424  neibastop2lem  28425  neibastop3  28427  prdstotbnd  28537  heibor1lem  28552  ispridl2  28682  elrfirn2  28877  rabdiophlem1  28984  dford3lem1  29220  kelac1  29261  acsfn1p  29401  climinf  29625  usg2wlkeq  30135  wwlknred  30201  wwlkm1edg  30213  clwlkisclwwlklem1  30295  clwwlkf  30302  wwlksubclwwlk  30312  extwwlkfablem2  30517  ssralv2  30937  ssralv2VD  31304  bnj1118  31677
  Copyright terms: Public domain W3C validator