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

Theorem rspccv 3207
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 3206 . 2  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
32com12 31 1  |-  ( A. x  e.  B  ph  ->  ( A  e.  B  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1395    e. wcel 1819   A.wral 2807
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-v 3111
This theorem is referenced by:  elinti  4297  fvn0ssdmfun  6023  dff3  6045  2fvcoidd  6201  ofrval  6549  limsuc  6683  limuni3  6686  frxp  6909  smo11  7053  odi  7246  supub  7936  suplub  7937  elirrv  8041  dfom3  8081  noinfep  8093  oemapvali  8120  tcrank  8319  infxpenlem  8408  alephle  8486  dfac5lem5  8525  dfac2  8528  cofsmo  8666  coftr  8670  infpssrlem4  8703  isf34lem6  8777  axcc2lem  8833  domtriomlem  8839  axdc2lem  8845  axdc3lem2  8848  axdc4lem  8852  ac5b  8875  zorn2lem2  8894  zorn2lem6  8898  pwcfsdom  8975  inar1  9170  grupw  9190  grupr  9192  gruurn  9193  grothpw  9221  grothpwex  9222  axgroth6  9223  grothomex  9224  nqereu  9324  supsrlem  9505  axpre-sup  9563  dedekind  9761  dedekindle  9762  supmullem1  10529  supmul  10531  peano5nni  10559  dfnn2  10569  peano5uzi  10972  zindd  10986  1arith  14457  ramcl  14559  clatleglb  15883  pslem  15963  mndassOLD  16059  cygabl  17020  eqcoe1ply1eq  18466  psgndiflemA  18764  mvmumamul1  19183  smadiadetlem0  19290  chpscmat  19470  basis2  19579  tg2  19593  clsndisj  19703  cnpimaex  19884  t1sncld  19954  regsep  19962  nrmsep3  19983  cmpsub  20027  2ndc1stc  20078  refssex  20138  ptfinfin  20146  txcnpi  20235  txcmplem1  20268  tx1stc  20277  filss  20480  ufilss  20532  fclsopni  20642  fclsrest  20651  alexsubb  20672  alexsubALTlem2  20674  alexsubALTlem4  20676  ghmcnp  20739  qustgplem  20745  mopni  21121  metrest  21153  metcnpi  21173  metcnpi2  21174  cfilucfilOLD  21198  cfilucfil  21199  nmolb  21350  nmoleub2lem2  21725  ovoliunlem1  22039  ovolicc2lem3  22056  mblsplit  22069  fta1b  22696  plycj  22800  mtest  22925  sqfpc  23537  ostth2lem2  23945  ostth3  23949  vdiscusgra  25048  rusgranumwwlkl1  25073  usgn0fidegnn0  25156  numclwwlk1  25225  lpni  25308  nvz  25699  ubthlem2  25914  chcompl  26287  ocin  26341  hmopidmchi  27197  dmdmd  27346  dmdbr5  27354  mdsl1i  27367  sigaclci  28305  lgamgulmlem1  28768  kur14lem9  28855  sconpht  28871  cvmsdisj  28912  untelirr  29298  untsucf  29300  dfon2lem4  29435  dfon2lem6  29437  dfon2lem7  29438  dfon2lem8  29439  dfon2  29441  wfrlem9  29568  frrlem5e  29612  sltval2  29633  heibor1lem  30510  heiborlem4  30515  heiborlem6  30517  stoweid  32048  bnj23  33914  atlex  35184  psubspi  35614  elpcliN  35760  ldilval  35980  trlord  36438  tendotp  36630  hdmapval2  37705  pwelg  37905
  Copyright terms: Public domain W3C validator