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

Theorem rspccv 2894
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 2893 . 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 1632    e. wcel 1696   A.wral 2556
This theorem is referenced by:  elinti  3887  limsuc  4656  limuni3  4659  dff3  5689  ofrval  6104  frxp  6241  smo11  6397  abianfp  6487  odi  6593  supub  7226  suplub  7227  elirrv  7327  dfom3  7364  noinfep  7376  oemapvali  7402  tcrank  7570  infxpenlem  7657  alephle  7731  dfac5lem5  7770  dfac2  7773  cofsmo  7911  coftr  7915  infpssrlem4  7948  isf34lem6  8022  axcc2lem  8078  domtriomlem  8084  axdc2lem  8090  axdc3lem2  8093  axdc4lem  8097  ac5b  8121  zorn2lem2  8140  zorn2lem6  8144  pwcfsdom  8221  inar1  8413  grupw  8433  grupr  8435  gruurn  8436  grothpw  8464  grothpwex  8465  axgroth6  8466  grothomex  8467  nqereu  8569  supsrlem  8749  axpre-sup  8807  supmullem1  9736  supmul  9738  peano5nni  9765  dfnn2  9775  peano5uzi  10116  zindd  10129  1arith  12990  ramcl  13092  luble  14131  glble  14136  joinle  14143  meetle  14150  clatleglb  14246  pslem  14331  cygabl  15193  basis2  16705  tg2  16719  clsndisj  16828  cnpimaex  17002  t1sncld  17070  regsep  17078  nrmsep3  17099  cmpsub  17143  2ndc1stc  17193  txcnpi  17318  txcmplem1  17351  tx1stc  17360  filss  17564  ufilss  17616  fclsopni  17726  fclsrest  17735  alexsubb  17756  alexsubALTlem2  17758  alexsubALTlem4  17760  ghmcnp  17813  divstgplem  17819  mopni  18054  metrest  18086  metcnpi  18106  metcnpi2  18107  nmolb  18242  nmoleub2lem2  18613  ovoliunlem1  18877  ovolicc2lem3  18894  mblsplit  18907  fta1b  19571  plycj  19674  mtest  19797  sqfpc  20391  ostth2lem2  20799  ostth3  20803  lpni  20862  nvz  21251  ubthlem2  21466  chcompl  21838  ocin  21891  hmopidmchi  22747  dmdmd  22896  dmdbr5  22904  mdsl1i  22917  kur14lem9  23760  sconpht  23775  cvmsdisj  23816  untelirr  24069  untsucf  24071  dedekind  24097  dedekindle  24098  dfon2lem4  24213  dfon2lem6  24215  dfon2lem7  24216  dfon2lem8  24217  dfon2  24219  wfrlem9  24335  frrlem5e  24360  sltval2  24381  domintreflemb  25165  preoref22  25332  svli2  25587  limptlimpr2lem1  25677  idosd  25847  refssex  26384  ptfinfin  26401  heibor1lem  26636  heiborlem4  26641  heiborlem6  26643  stoweid  27915  bnj23  29060  atlex  30128  psubspi  30558  elpcliN  30704  ldilval  30924  trlord  31380  tendotp  31572  hdmapval2  32647
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-v 2803
  Copyright terms: Public domain W3C validator