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

Theorem rspccv 3059
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 3058 . 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 1362    e. wcel 1755   A.wral 2705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ral 2710  df-v 2964
This theorem is referenced by:  elinti  4125  dff3  5844  ofrval  6319  limsuc  6449  limuni3  6452  frxp  6671  smo11  6811  abianfp  6900  odi  7006  supub  7697  suplub  7698  elirrv  7800  dfom3  7841  noinfep  7853  oemapvali  7880  tcrank  8079  infxpenlem  8168  alephle  8246  dfac5lem5  8285  dfac2  8288  cofsmo  8426  coftr  8430  infpssrlem4  8463  isf34lem6  8537  axcc2lem  8593  domtriomlem  8599  axdc2lem  8605  axdc3lem2  8608  axdc4lem  8612  ac5b  8635  zorn2lem2  8654  zorn2lem6  8658  pwcfsdom  8735  inar1  8929  grupw  8949  grupr  8951  gruurn  8952  grothpw  8980  grothpwex  8981  axgroth6  8982  grothomex  8983  nqereu  9085  supsrlem  9265  axpre-sup  9323  dedekind  9520  dedekindle  9521  supmullem1  10283  supmul  10285  peano5nni  10312  dfnn2  10322  peano5uzi  10717  zindd  10730  1arith  13970  ramcl  14072  clatleglb  15278  pslem  15358  cygabl  16346  psgndiflemA  17872  smadiadetlem0  18308  basis2  18397  tg2  18411  clsndisj  18520  cnpimaex  18701  t1sncld  18771  regsep  18779  nrmsep3  18800  cmpsub  18844  2ndc1stc  18896  txcnpi  19022  txcmplem1  19055  tx1stc  19064  filss  19267  ufilss  19319  fclsopni  19429  fclsrest  19438  alexsubb  19459  alexsubALTlem2  19461  alexsubALTlem4  19463  ghmcnp  19526  divstgplem  19532  mopni  19908  metrest  19940  metcnpi  19960  metcnpi2  19961  cfilucfilOLD  19985  cfilucfil  19986  nmolb  20137  nmoleub2lem2  20512  ovoliunlem1  20826  ovolicc2lem3  20843  mblsplit  20856  fta1b  21525  plycj  21628  mtest  21753  sqfpc  22359  ostth2lem2  22767  ostth3  22771  lpni  23488  nvz  23879  ubthlem2  24094  chcompl  24467  ocin  24521  hmopidmchi  25377  dmdmd  25526  dmdbr5  25534  mdsl1i  25547  sigaclci  26428  lgamgulmlem1  26862  kur14lem9  26949  sconpht  26965  cvmsdisj  27006  untelirr  27205  untsucf  27207  dfon2lem4  27445  dfon2lem6  27447  dfon2lem7  27448  dfon2lem8  27449  dfon2  27451  wfrlem9  27578  frrlem5e  27622  sltval2  27643  refssex  28394  ptfinfin  28411  heibor1lem  28549  heiborlem4  28554  heiborlem6  28556  stoweid  29701  bnj23  31406  atlex  32531  psubspi  32961  elpcliN  33107  ldilval  33327  trlord  33783  tendotp  33975  hdmapval2  35050
  Copyright terms: Public domain W3C validator