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

Theorem ssralv 3250
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 3187 . . 3  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21imim1d 69 . 2  |-  ( A 
C_  B  ->  (
( x  e.  B  ->  ph )  ->  (
x  e.  A  ->  ph ) ) )
32ralimdv2 2636 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 1696   A.wral 2556    C_ wss 3165
This theorem is referenced by:  iinss1  3933  disjiun  4029  poss  4332  sess2  4378  isores3  5848  isoini2  5852  smores  6385  smores2  6387  tfrlem1  6407  resixp  6867  ac6sfi  7117  iunfi  7160  ixpfi2  7170  dffi3  7200  marypha1lem  7202  ordtypelem2  7250  tcrank  7570  acndom  7694  pwsdompw  7846  ssfin3ds  7972  fin1a2s  8056  hsmexlem4  8071  domtriomlem  8084  zornn0g  8148  fpwwe2lem13  8280  ingru  8453  rexanuz  11845  cau3lem  11854  caubnd  11858  limsupgord  11962  limsupval2  11970  rlimres  12048  lo1res  12049  o1of2  12102  o1rlimmul  12108  isercolllem1  12154  climsup  12159  fsumiun  12295  pcfac  12963  vdwnnlem2  13059  firest  13353  imasaddfnlem  13446  imasvscafn  13455  psss  14339  tsrss  14348  cntz2ss  14824  cntzmhm2  14831  subgpgp  14924  efgsres  15063  dprdss  15280  ocv2ss  16589  mretopd  16845  tgcn  16998  tgcnp  16999  subbascn  17000  cnss2  17022  cncnp  17025  sslm  17043  t1ficld  17071  tgcmp  17144  1stcfb  17187  islly2  17226  dislly  17239  ptbasfi  17292  ptcnplem  17331  tx1stc  17360  qtoptop2  17406  fbunfip  17580  flftg  17707  txflf  17717  fclsbas  17732  fclsss1  17733  fclsss2  17734  alexsubb  17756  tmdgsum2  17795  metrest  18086  rescncf  18417  cnllycmp  18470  bndth  18472  fgcfil  18713  cfilres  18738  ivthlem2  18828  ivthlem3  18829  ovolsslem  18859  ovolfiniun  18876  finiunmbl  18917  volfiniun  18920  iunmbl  18926  ioombl1lem4  18934  dyadmax  18969  vitali  18984  mbfimaopnlem  19026  mbflimsup  19037  mbfi1flim  19094  ditgeq3  19216  dvferm  19351  rollelem  19352  dvivthlem1  19371  itgsubstlem  19411  aalioulem2  19729  ulmcaulem  19787  ulmss  19790  xrlimcnp  20279  lgsdchr  20603  pntlem3  20774  pntlemp  20775  pntleml  20776  occon  21882  sigaclci  23508  measiun  23560  elmbfmvol2  23587  subfacp1lem3  23728  iccllyscon  23796  untint  24073  untangtr  24075  dfon2lem6  24215  dfon2lem8  24217  dfon2lem9  24218  setlikess  24266  poseq  24324  soseq  24325  ubpar  25364  lvsovso3  25731  comppfsc  26410  neibastop1  26411  neibastop2lem  26412  neibastop3  26414  prdstotbnd  26621  heibor1lem  26636  ispridl2  26766  elrfirn2  26874  rabdiophlem1  26985  dford3lem1  27222  kelac1  27264  acsfn1p  27610  climinf  27835  redwlk  28364  ssralv2  28593  ssralv2VD  28958  bnj1118  29330
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-ral 2561  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator