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

Theorem rspccv 2881
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 2880 . 2  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
32com12 27 1  |-  ( A. x  e.  B  ph  ->  ( A  e.  B  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623    e. wcel 1684   A.wral 2543
This theorem is referenced by:  elinti  3871  limsuc  4640  limuni3  4643  dff3  5673  ofrval  6088  frxp  6225  smo11  6381  abianfp  6471  odi  6577  supub  7210  suplub  7211  elirrv  7311  dfom3  7348  noinfep  7360  oemapvali  7386  tcrank  7554  infxpenlem  7641  alephle  7715  dfac5lem5  7754  dfac2  7757  cofsmo  7895  coftr  7899  infpssrlem4  7932  isf34lem6  8006  axcc2lem  8062  domtriomlem  8068  axdc2lem  8074  axdc3lem2  8077  axdc4lem  8081  ac5b  8105  zorn2lem2  8124  zorn2lem6  8128  pwcfsdom  8205  inar1  8397  grupw  8417  grupr  8419  gruurn  8420  grothpw  8448  grothpwex  8449  axgroth6  8450  grothomex  8451  nqereu  8553  supsrlem  8733  axpre-sup  8791  supmullem1  9720  supmul  9722  peano5nni  9749  dfnn2  9759  peano5uzi  10100  zindd  10113  1arith  12974  ramcl  13076  luble  14115  glble  14120  joinle  14127  meetle  14134  clatleglb  14230  pslem  14315  cygabl  15177  basis2  16689  tg2  16703  clsndisj  16812  cnpimaex  16986  t1sncld  17054  regsep  17062  nrmsep3  17083  cmpsub  17127  2ndc1stc  17177  txcnpi  17302  txcmplem1  17335  tx1stc  17344  filss  17548  ufilss  17600  fclsopni  17710  fclsrest  17719  alexsubb  17740  alexsubALTlem2  17742  alexsubALTlem4  17744  ghmcnp  17797  divstgplem  17803  mopni  18038  metrest  18070  metcnpi  18090  metcnpi2  18091  nmolb  18226  nmoleub2lem2  18597  ovoliunlem1  18861  ovolicc2lem3  18878  mblsplit  18891  fta1b  19555  plycj  19658  mtest  19781  sqfpc  20375  ostth2lem2  20783  ostth3  20787  lpni  20846  nvz  21235  ubthlem2  21450  chcompl  21822  ocin  21875  hmopidmchi  22731  dmdmd  22880  dmdbr5  22888  mdsl1i  22901  kur14lem9  23745  sconpht  23760  cvmsdisj  23801  untelirr  24054  untsucf  24056  dedekind  24082  dedekindle  24083  dfon2lem4  24142  dfon2lem6  24144  dfon2lem7  24145  dfon2lem8  24146  dfon2  24148  wfrlem9  24264  frrlem5e  24289  sltval2  24310  domintreflemb  25062  preoref22  25229  svli2  25484  limptlimpr2lem1  25574  idosd  25744  refssex  26281  ptfinfin  26298  heibor1lem  26533  heiborlem4  26538  heiborlem6  26540  stoweid  27812  bnj23  28744  atlex  29506  psubspi  29936  elpcliN  30082  ldilval  30302  trlord  30758  tendotp  30950  hdmapval2  32025
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-v 2790
  Copyright terms: Public domain W3C validator