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

Theorem ssralv 3343
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 3278 . . 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 2722 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 1717   A.wral 2642    C_ wss 3256
This theorem is referenced by:  iinss1  4040  disjiun  4136  poss  4439  sess2  4485  isores3  5987  isoini2  5991  smores  6543  smores2  6545  tfrlem1  6565  resixp  7026  ac6sfi  7280  iunfi  7323  ixpfi2  7333  dffi3  7364  marypha1lem  7366  ordtypelem2  7414  tcrank  7734  acndom  7858  pwsdompw  8010  ssfin3ds  8136  fin1a2s  8220  hsmexlem4  8235  domtriomlem  8248  zornn0g  8311  fpwwe2lem13  8443  ingru  8616  rexanuz  12069  cau3lem  12078  caubnd  12082  limsupgord  12186  limsupval2  12194  rlimres  12272  lo1res  12273  o1of2  12326  o1rlimmul  12332  isercolllem1  12378  climsup  12383  fsumiun  12520  pcfac  13188  vdwnnlem2  13284  firest  13580  imasaddfnlem  13673  imasvscafn  13682  psss  14566  tsrss  14575  cntz2ss  15051  cntzmhm2  15058  subgpgp  15151  efgsres  15290  dprdss  15507  ocv2ss  16816  mretopd  17072  tgcn  17231  tgcnp  17232  subbascn  17233  cnss2  17256  cncnp  17259  sslm  17278  t1ficld  17306  tgcmp  17379  1stcfb  17422  islly2  17461  dislly  17474  ptbasfi  17527  ptcnplem  17567  tx1stc  17596  qtoptop2  17645  fbunfip  17815  flftg  17942  txflf  17952  fclsbas  17967  fclsss1  17968  fclsss2  17969  alexsubb  17991  tmdgsum2  18040  metrest  18437  rescncf  18791  cnllycmp  18845  bndth  18847  fgcfil  19088  cfilres  19113  ivthlem2  19209  ivthlem3  19210  ovolsslem  19240  ovolfiniun  19257  finiunmbl  19298  volfiniun  19301  iunmbl  19307  ioombl1lem4  19315  dyadmax  19350  vitali  19365  mbfimaopnlem  19407  mbflimsup  19418  mbfi1flim  19475  ditgeq3  19597  dvferm  19732  rollelem  19733  dvivthlem1  19752  itgsubstlem  19792  aalioulem2  20110  ulmcaulem  20170  ulmss  20173  xrlimcnp  20667  lgsdchr  20992  pntlem3  21163  pntlemp  21164  pntleml  21165  nbgraf1olem1  21310  redwlk  21447  occon  22630  resspos  24019  resstos  24020  sigaclci  24304  measiun  24359  elmbfmvol2  24404  subfacp1lem3  24640  iccllyscon  24709  untint  24933  untangtr  24935  dfon2lem6  25161  dfon2lem8  25163  dfon2lem9  25164  setlikess  25212  poseq  25270  soseq  25271  volsupnfl  25949  comppfsc  26071  neibastop1  26072  neibastop2lem  26073  neibastop3  26075  prdstotbnd  26187  heibor1lem  26202  ispridl2  26332  elrfirn2  26434  rabdiophlem1  26545  dford3lem1  26781  kelac1  26823  acsfn1p  27169  climinf  27393  ssralv2  27951  ssralv2VD  28312  bnj1118  28684
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
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 2367  df-cleq 2373  df-clel 2376  df-ral 2647  df-in 3263  df-ss 3270
  Copyright terms: Public domain W3C validator