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

Theorem ssralv 3411
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 3345 . . 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 2791 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 1756   A.wral 2710    C_ wss 3323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-ral 2715  df-in 3330  df-ss 3337
This theorem is referenced by:  iinss1  4178  disjiun  4277  poss  4638  sess2  4684  isores3  6021  isoini2  6025  smores  6805  smores2  6807  tfrlem5  6831  resixp  7290  ac6sfi  7548  iunfi  7591  ixpfi2  7601  dffi3  7673  marypha1lem  7675  ordtypelem2  7725  tcrank  8083  acndom  8213  pwsdompw  8365  ssfin3ds  8491  fin1a2s  8575  hsmexlem4  8590  domtriomlem  8603  zornn0g  8666  fpwwe2lem13  8801  ingru  8974  cshw1  12448  rexanuz  12825  cau3lem  12834  caubnd  12838  limsupgord  12942  limsupval2  12950  rlimres  13028  lo1res  13029  o1of2  13082  o1rlimmul  13088  isercolllem1  13134  climsup  13139  fsumiun  13276  pcfac  13953  vdwnnlem2  14049  firest  14363  imasaddfnlem  14458  imasvscafn  14467  psss  15376  tsrss  15385  cntz2ss  15841  cntzmhm2  15848  subgpgp  16087  efgsres  16226  dprdss  16516  ocv2ss  18078  mretopd  18676  tgcn  18836  tgcnp  18837  subbascn  18838  cnss2  18861  cncnp  18864  sslm  18883  t1ficld  18911  tgcmp  18984  1stcfb  19029  islly2  19068  dislly  19081  ptbasfi  19134  ptcnplem  19174  tx1stc  19203  qtoptop2  19252  fbunfip  19422  flftg  19549  txflf  19559  fclsbas  19574  fclsss1  19575  fclsss2  19576  alexsubb  19598  tmdgsum2  19647  metrest  20079  rescncf  20453  cnllycmp  20508  bndth  20510  fgcfil  20762  cfilres  20787  ivthlem2  20916  ivthlem3  20917  ovolsslem  20947  ovolfiniun  20964  finiunmbl  21005  volfiniun  21008  iunmbl  21014  ioombl1lem4  21022  dyadmax  21058  vitali  21073  mbfimaopnlem  21113  mbflimsup  21124  mbfi1flim  21181  ditgeq3  21305  dvferm  21440  rollelem  21441  dvivthlem1  21460  itgsubstlem  21500  aalioulem2  21779  ulmcaulem  21839  ulmss  21842  xrlimcnp  22342  lgsdchr  22667  pntlem3  22838  pntlemp  22839  pntleml  22840  nbgraf1olem1  23318  redwlk  23473  occon  24658  xrge0infss  26021  resspos  26088  resstos  26089  submarchi  26171  sigaclci  26544  measiun  26601  elmbfmvol2  26651  sibfof  26695  subfacp1lem3  27039  iccllyscon  27108  untint  27332  untangtr  27334  dfon2lem6  27570  dfon2lem8  27572  dfon2lem9  27573  setlikess  27625  poseq  27683  soseq  27684  finixpnum  28385  heicant  28397  volsupnfl  28407  comppfsc  28550  neibastop1  28551  neibastop2lem  28552  neibastop3  28554  prdstotbnd  28664  heibor1lem  28679  ispridl2  28809  elrfirn2  29003  rabdiophlem1  29110  dford3lem1  29346  kelac1  29387  acsfn1p  29527  climinf  29750  usg2wlkeq  30260  wwlknred  30326  wwlkm1edg  30338  clwlkisclwwlklem1  30420  clwwlkf  30427  wwlksubclwwlk  30437  extwwlkfablem2  30642  ssralv2  31165  ssralv2VD  31531  bnj1118  31904
  Copyright terms: Public domain W3C validator