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

Theorem rspccv 3009
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 2-Feb-2006.)
Hypothesis
Ref Expression
rspcv.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
rspccv  |-  ( A. x  e.  B  ph  ->  ( A  e.  B  ->  ps ) )
Distinct variable groups:    x, A    x, B    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem rspccv
StepHypRef Expression
1 rspcv.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
21rspcv 3008 . 2  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
32com12 29 1  |-  ( A. x  e.  B  ph  ->  ( A  e.  B  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649    e. wcel 1721   A.wral 2666
This theorem is referenced by:  elinti  4019  limsuc  4788  limuni3  4791  dff3  5841  ofrval  6274  frxp  6415  smo11  6585  abianfp  6675  odi  6781  supub  7420  suplub  7421  elirrv  7521  dfom3  7558  noinfep  7570  oemapvali  7596  tcrank  7764  infxpenlem  7851  alephle  7925  dfac5lem5  7964  dfac2  7967  cofsmo  8105  coftr  8109  infpssrlem4  8142  isf34lem6  8216  axcc2lem  8272  domtriomlem  8278  axdc2lem  8284  axdc3lem2  8287  axdc4lem  8291  ac5b  8314  zorn2lem2  8333  zorn2lem6  8337  pwcfsdom  8414  inar1  8606  grupw  8626  grupr  8628  gruurn  8629  grothpw  8657  grothpwex  8658  axgroth6  8659  grothomex  8660  nqereu  8762  supsrlem  8942  axpre-sup  9000  supmullem1  9930  supmul  9932  peano5nni  9959  dfnn2  9969  peano5uzi  10314  zindd  10327  1arith  13250  ramcl  13352  luble  14393  glble  14398  joinle  14405  meetle  14412  clatleglb  14508  pslem  14593  cygabl  15455  basis2  16971  tg2  16985  clsndisj  17094  cnpimaex  17274  t1sncld  17344  regsep  17352  nrmsep3  17373  cmpsub  17417  2ndc1stc  17467  txcnpi  17593  txcmplem1  17626  tx1stc  17635  filss  17838  ufilss  17890  fclsopni  18000  fclsrest  18009  alexsubb  18030  alexsubALTlem2  18032  alexsubALTlem4  18034  ghmcnp  18097  divstgplem  18103  mopni  18475  metrest  18507  metcnpi  18527  metcnpi2  18528  cfilucfilOLD  18552  cfilucfil  18553  nmolb  18704  nmoleub2lem2  19077  ovoliunlem1  19351  ovolicc2lem3  19368  mblsplit  19381  fta1b  20045  plycj  20148  mtest  20273  sqfpc  20873  ostth2lem2  21281  ostth3  21285  lpni  21720  nvz  22111  ubthlem2  22326  chcompl  22698  ocin  22751  hmopidmchi  23607  dmdmd  23756  dmdbr5  23764  mdsl1i  23777  sigaclci  24468  lgamgulmlem1  24766  kur14lem9  24853  sconpht  24869  cvmsdisj  24910  untelirr  25110  untsucf  25112  dedekind  25140  dedekindle  25141  dfon2lem4  25356  dfon2lem6  25358  dfon2lem7  25359  dfon2lem8  25360  dfon2  25362  wfrlem9  25478  frrlem5e  25503  sltval2  25524  refssex  26251  ptfinfin  26268  heibor1lem  26408  heiborlem4  26413  heiborlem6  26415  stoweid  27679  bnj23  28789  atlex  29799  psubspi  30229  elpcliN  30375  ldilval  30595  trlord  31051  tendotp  31243  hdmapval2  32318
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-nfc 2529  df-ral 2671  df-v 2918
  Copyright terms: Public domain W3C validator