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

Theorem ssralv 3525
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 3458 . . 3  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21imim1d 78 . 2  |-  ( A 
C_  B  ->  (
( x  e.  B  ->  ph )  ->  (
x  e.  A  ->  ph ) ) )
32ralimdv2 2832 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 1868   A.wral 2775    C_ wss 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-ral 2780  df-in 3443  df-ss 3450
This theorem is referenced by:  intss  4273  iinss1  4309  disjiun  4411  poss  4772  sess2  4818  isores3  6237  isoini2  6241  smores  7075  smores2  7077  tfrlem5  7102  resixp  7561  ac6sfi  7817  iunfi  7864  ixpfi2  7874  dffi3  7947  marypha1lem  7949  ordtypelem2  8036  tcrank  8356  acndom  8482  pwsdompw  8634  ssfin3ds  8760  fin1a2s  8844  hsmexlem4  8859  domtriomlem  8872  zornn0g  8935  fpwwe2lem13  9067  ingru  9240  cshw1  12909  rexanuz  13394  cau3lem  13403  caubnd  13407  limsupgord  13513  limsupval2  13525  limsupval2OLD  13526  rlimres  13607  lo1res  13608  o1of2  13661  o1rlimmul  13667  isercolllem1  13713  climsup  13718  fsumiun  13866  lcmfunsnlem1  14595  coprmprod  14663  pcfac  14829  vdwnnlem2  14931  firest  15316  imasaddfnlem  15419  imasvscafn  15428  psss  16445  tsrss  16454  cntz2ss  16971  cntzmhm2  16978  subgpgp  17234  efgsres  17373  telgsumfzs  17604  telgsums  17608  dprdss  17647  ocv2ss  19220  mretopd  20092  tgcn  20252  tgcnp  20253  subbascn  20254  cnss2  20277  cncnp  20280  sslm  20299  t1ficld  20327  tgcmp  20400  1stcfb  20444  islly2  20483  dislly  20496  comppfsc  20531  ptbasfi  20580  ptcnplem  20620  tx1stc  20649  qtoptop2  20698  fbunfip  20868  flftg  20995  txflf  21005  fclsbas  21020  fclsss1  21021  fclsss2  21022  alexsubb  21045  tmdgsum2  21095  metrest  21523  rescncf  21913  cnllycmp  21968  bndth  21970  fgcfil  22225  cfilres  22250  ivthlem2  22387  ivthlem3  22388  ovolsslem  22421  ovolfiniun  22438  finiunmbl  22481  volfiniun  22484  iunmbl  22490  ioombl1lem4  22498  dyadmax  22540  vitali  22555  mbfimaopnlem  22595  mbflimsup  22607  mbflimsupOLD  22608  mbfi1flim  22665  ditgeq3  22789  dvferm  22924  rollelem  22925  dvivthlem1  22944  itgsubstlem  22984  aalioulem2  23273  ulmcaulem  23333  ulmss  23336  xrlimcnp  23878  lgsdchr  24260  pntlem3  24431  pntlemp  24432  pntleml  24433  nbgraf1olem1  25152  redwlk  25319  usg2wlkeq  25419  wwlknred  25434  wwlkm1edg  25446  clwlkisclwwlklem1  25498  clwwlkf  25505  wwlksubclwwlk  25515  extwwlkfablem2  25789  occon  26923  xrge0infss  28331  xrge0infssOLD  28332  resspos  28412  resstos  28413  submarchi  28495  sigaclci  28947  measiun  29033  elmbfmvol2  29082  sibfof  29166  bnj1118  29786  subfacp1lem3  29898  iccllyscon  29966  untint  30332  untangtr  30334  dfon2lem6  30426  dfon2lem8  30428  dfon2lem9  30429  poseq  30483  soseq  30484  neibastop1  31005  neibastop2lem  31006  neibastop3  31008  finixpnum  31841  ptrecube  31851  poimirlem26  31877  poimirlem27  31878  poimirlem30  31881  heicant  31886  volsupnfl  31896  prdstotbnd  32037  heibor1lem  32052  ispridl2  32182  elrfirn2  35454  rabdiophlem1  35560  dford3lem1  35798  kelac1  35838  acsfn1p  35982  ssralv2  36743  ssralv2VD  37121  climinf  37501  climinfOLD  37502  iccpartres  38441
  Copyright terms: Public domain W3C validator