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

Theorem rspccv 3147
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 3146 . 2  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
32com12 32 1  |-  ( A. x  e.  B  ph  ->  ( A  e.  B  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    = wceq 1444    e. wcel 1887   A.wral 2737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ral 2742  df-v 3047
This theorem is referenced by:  elinti  4243  fvn0ssdmfun  6013  dff3  6035  2fvcoidd  6195  ofrval  6541  limsuc  6676  limuni3  6679  frxp  6906  wfrdmcl  7044  smo11  7083  odi  7280  supub  7973  suplub  7974  elirrv  8112  dfom3  8152  noinfep  8165  oemapvali  8189  tcrank  8355  infxpenlem  8444  alephle  8519  dfac5lem5  8558  dfac2  8561  cofsmo  8699  coftr  8703  infpssrlem4  8736  isf34lem6  8810  axcc2lem  8866  domtriomlem  8872  axdc2lem  8878  axdc3lem2  8881  axdc4lem  8885  ac5b  8908  zorn2lem2  8927  zorn2lem6  8931  pwcfsdom  9008  inar1  9200  grupw  9220  grupr  9222  gruurn  9223  grothpw  9251  grothpwex  9252  axgroth6  9253  grothomex  9254  nqereu  9354  supsrlem  9535  axpre-sup  9593  dedekind  9797  dedekindle  9798  supmullem1  10577  supmul  10579  peano5nni  10612  dfnn2  10622  peano5uzi  11024  zindd  11036  1arith  14871  ramcl  14987  clatleglb  16372  pslem  16452  mndassOLD  16548  cygabl  17525  eqcoe1ply1eq  18891  psgndiflemA  19169  mvmumamul1  19579  smadiadetlem0  19686  chpscmat  19866  basis2  19966  tg2  19980  clsndisj  20091  cnpimaex  20272  t1sncld  20342  regsep  20350  nrmsep3  20371  cmpsub  20415  2ndc1stc  20466  refssex  20526  ptfinfin  20534  txcnpi  20623  txcmplem1  20656  tx1stc  20665  filss  20868  ufilss  20920  fclsopni  21030  fclsrest  21039  alexsubb  21061  alexsubALTlem2  21063  alexsubALTlem4  21065  ghmcnp  21129  qustgplem  21135  mopni  21507  metrest  21539  metcnpi  21559  metcnpi2  21560  cfilucfil  21574  nmolb  21722  nmolbOLD  21741  nmoleub2lem2  22130  ovoliunlem1  22455  ovolicc2lem3  22472  mblsplit  22486  fta1b  23120  plycj  23231  mtest  23359  lgamgulmlem1  23954  sqfpc  24064  ostth2lem2  24472  ostth3  24476  vdiscusgra  25649  rusgranumwwlkl1  25674  usgn0fidegnn0  25757  numclwwlk1  25826  lpni  25911  nvz  26298  ubthlem2  26513  chcompl  26895  ocin  26949  hmopidmchi  27804  dmdmd  27953  dmdbr5  27961  mdsl1i  27974  sigaclci  28954  bnj23  29524  kur14lem9  29937  sconpht  29952  cvmsdisj  29993  untelirr  30335  untsucf  30337  dfon2lem4  30432  dfon2lem6  30434  dfon2lem7  30435  dfon2lem8  30436  dfon2  30438  frrlem5e  30522  sltval2  30543  fwddifnp1  30932  poimirlem18  31958  poimirlem21  31961  heibor1lem  32141  heiborlem4  32146  heiborlem6  32148  atlex  32882  psubspi  33312  elpcliN  33458  ldilval  33678  trlord  34136  tendotp  34328  hdmapval2  35403  pwelg  36164  stoweid  37925  iccpartltu  38739  iccpartgtl  38740  iccpartleu  38742  iccpartgel  38743  nbgrnself2  39431  vdiscusgr  39568  ewlkinedg  39621
  Copyright terms: Public domain W3C validator