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

Theorem ssralv 3367
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 3302 . . 3  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21imim1d 71 . 2  |-  ( A 
C_  B  ->  (
( x  e.  B  ->  ph )  ->  (
x  e.  A  ->  ph ) ) )
32ralimdv2 2746 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 1721   A.wral 2666    C_ wss 3280
This theorem is referenced by:  iinss1  4065  disjiun  4162  poss  4465  sess2  4511  isores3  6014  isoini2  6018  smores  6573  smores2  6575  tfrlem1  6595  resixp  7056  ac6sfi  7310  iunfi  7353  ixpfi2  7363  dffi3  7394  marypha1lem  7396  ordtypelem2  7444  tcrank  7764  acndom  7888  pwsdompw  8040  ssfin3ds  8166  fin1a2s  8250  hsmexlem4  8265  domtriomlem  8278  zornn0g  8341  fpwwe2lem13  8473  ingru  8646  rexanuz  12104  cau3lem  12113  caubnd  12117  limsupgord  12221  limsupval2  12229  rlimres  12307  lo1res  12308  o1of2  12361  o1rlimmul  12367  isercolllem1  12413  climsup  12418  fsumiun  12555  pcfac  13223  vdwnnlem2  13319  firest  13615  imasaddfnlem  13708  imasvscafn  13717  psss  14601  tsrss  14610  cntz2ss  15086  cntzmhm2  15093  subgpgp  15186  efgsres  15325  dprdss  15542  ocv2ss  16855  mretopd  17111  tgcn  17270  tgcnp  17271  subbascn  17272  cnss2  17295  cncnp  17298  sslm  17317  t1ficld  17345  tgcmp  17418  1stcfb  17461  islly2  17500  dislly  17513  ptbasfi  17566  ptcnplem  17606  tx1stc  17635  qtoptop2  17684  fbunfip  17854  flftg  17981  txflf  17991  fclsbas  18006  fclsss1  18007  fclsss2  18008  alexsubb  18030  tmdgsum2  18079  metrest  18507  rescncf  18880  cnllycmp  18934  bndth  18936  fgcfil  19177  cfilres  19202  ivthlem2  19302  ivthlem3  19303  ovolsslem  19333  ovolfiniun  19350  finiunmbl  19391  volfiniun  19394  iunmbl  19400  ioombl1lem4  19408  dyadmax  19443  vitali  19458  mbfimaopnlem  19500  mbflimsup  19511  mbfi1flim  19568  ditgeq3  19690  dvferm  19825  rollelem  19826  dvivthlem1  19845  itgsubstlem  19885  aalioulem2  20203  ulmcaulem  20263  ulmss  20266  xrlimcnp  20760  lgsdchr  21085  pntlem3  21256  pntlemp  21257  pntleml  21258  nbgraf1olem1  21404  redwlk  21559  occon  22742  resspos  24140  resstos  24141  sigaclci  24468  measiun  24525  elmbfmvol2  24570  sibfof  24607  subfacp1lem3  24821  iccllyscon  24890  untint  25114  untangtr  25116  dfon2lem6  25358  dfon2lem8  25360  dfon2lem9  25361  setlikess  25409  poseq  25467  soseq  25468  volsupnfl  26150  comppfsc  26277  neibastop1  26278  neibastop2lem  26279  neibastop3  26281  prdstotbnd  26393  heibor1lem  26408  ispridl2  26538  elrfirn2  26640  rabdiophlem1  26751  dford3lem1  26987  kelac1  27029  acsfn1p  27375  climinf  27599  ssralv2  28326  ssralv2VD  28687  bnj1118  29059
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-ral 2671  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator