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

Theorem ssralv 3409
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 3344 . . 3  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21imim1d 72 . 2  |-  ( A 
C_  B  ->  (
( x  e.  B  ->  ph )  ->  (
x  e.  A  ->  ph ) ) )
32ralimdv2 2788 1  |-  ( A 
C_  B  ->  ( A. x  e.  B  ph 
->  A. x  e.  A  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   A.wral 2707    C_ wss 3322
This theorem is referenced by:  iinss1  4107  disjiun  4205  poss  4508  sess2  4554  isores3  6058  isoini2  6062  smores  6617  smores2  6619  tfrlem1  6639  resixp  7100  ac6sfi  7354  iunfi  7397  ixpfi2  7408  dffi3  7439  marypha1lem  7441  ordtypelem2  7491  tcrank  7813  acndom  7937  pwsdompw  8089  ssfin3ds  8215  fin1a2s  8299  hsmexlem4  8314  domtriomlem  8327  zornn0g  8390  fpwwe2lem13  8522  ingru  8695  rexanuz  12154  cau3lem  12163  caubnd  12167  limsupgord  12271  limsupval2  12279  rlimres  12357  lo1res  12358  o1of2  12411  o1rlimmul  12417  isercolllem1  12463  climsup  12468  fsumiun  12605  pcfac  13273  vdwnnlem2  13369  firest  13665  imasaddfnlem  13758  imasvscafn  13767  psss  14651  tsrss  14660  cntz2ss  15136  cntzmhm2  15143  subgpgp  15236  efgsres  15375  dprdss  15592  ocv2ss  16905  mretopd  17161  tgcn  17321  tgcnp  17322  subbascn  17323  cnss2  17346  cncnp  17349  sslm  17368  t1ficld  17396  tgcmp  17469  1stcfb  17513  islly2  17552  dislly  17565  ptbasfi  17618  ptcnplem  17658  tx1stc  17687  qtoptop2  17736  fbunfip  17906  flftg  18033  txflf  18043  fclsbas  18058  fclsss1  18059  fclsss2  18060  alexsubb  18082  tmdgsum2  18131  metrest  18559  rescncf  18932  cnllycmp  18986  bndth  18988  fgcfil  19229  cfilres  19254  ivthlem2  19354  ivthlem3  19355  ovolsslem  19385  ovolfiniun  19402  finiunmbl  19443  volfiniun  19446  iunmbl  19452  ioombl1lem4  19460  dyadmax  19495  vitali  19510  mbfimaopnlem  19550  mbflimsup  19561  mbfi1flim  19618  ditgeq3  19742  dvferm  19877  rollelem  19878  dvivthlem1  19897  itgsubstlem  19937  aalioulem2  20255  ulmcaulem  20315  ulmss  20318  xrlimcnp  20812  lgsdchr  21137  pntlem3  21308  pntlemp  21309  pntleml  21310  nbgraf1olem1  21456  redwlk  21611  occon  22794  resspos  24192  resstos  24193  sigaclci  24520  measiun  24577  elmbfmvol2  24622  sibfof  24659  subfacp1lem3  24873  iccllyscon  24942  untint  25166  untangtr  25168  dfon2lem6  25420  dfon2lem8  25422  dfon2lem9  25423  setlikess  25475  poseq  25533  soseq  25534  heicant  26253  volsupnfl  26263  comppfsc  26401  neibastop1  26402  neibastop2lem  26403  neibastop3  26405  prdstotbnd  26517  heibor1lem  26532  ispridl2  26662  elrfirn2  26764  rabdiophlem1  26875  dford3lem1  27111  kelac1  27152  acsfn1p  27498  climinf  27722  cshw1  28309  usg2wlkeq  28342  ssralv2  28689  ssralv2VD  29052  bnj1118  29427
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-ral 2712  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator