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

Theorem rspccv 3051
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 3050 . 2  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
32com12 30 1  |-  ( A. x  e.  B  ph  ->  ( A  e.  B  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    = wceq 1653    e. wcel 1726   A.wral 2707
This theorem is referenced by:  elinti  4061  limsuc  4831  limuni3  4834  dff3  5884  ofrval  6317  frxp  6458  smo11  6628  abianfp  6718  odi  6824  supub  7466  suplub  7467  elirrv  7567  dfom3  7604  noinfep  7616  oemapvali  7642  tcrank  7810  infxpenlem  7897  alephle  7971  dfac5lem5  8010  dfac2  8013  cofsmo  8151  coftr  8155  infpssrlem4  8188  isf34lem6  8262  axcc2lem  8318  domtriomlem  8324  axdc2lem  8330  axdc3lem2  8333  axdc4lem  8337  ac5b  8360  zorn2lem2  8379  zorn2lem6  8383  pwcfsdom  8460  inar1  8652  grupw  8672  grupr  8674  gruurn  8675  grothpw  8703  grothpwex  8704  axgroth6  8705  grothomex  8706  nqereu  8808  supsrlem  8988  axpre-sup  9046  supmullem1  9976  supmul  9978  peano5nni  10005  dfnn2  10015  peano5uzi  10360  zindd  10373  1arith  13297  ramcl  13399  luble  14440  glble  14445  joinle  14452  meetle  14459  clatleglb  14555  pslem  14640  cygabl  15502  basis2  17018  tg2  17032  clsndisj  17141  cnpimaex  17322  t1sncld  17392  regsep  17400  nrmsep3  17421  cmpsub  17465  2ndc1stc  17516  txcnpi  17642  txcmplem1  17675  tx1stc  17684  filss  17887  ufilss  17939  fclsopni  18049  fclsrest  18058  alexsubb  18079  alexsubALTlem2  18081  alexsubALTlem4  18083  ghmcnp  18146  divstgplem  18152  mopni  18524  metrest  18556  metcnpi  18576  metcnpi2  18577  cfilucfilOLD  18601  cfilucfil  18602  nmolb  18753  nmoleub2lem2  19126  ovoliunlem1  19400  ovolicc2lem3  19417  mblsplit  19430  fta1b  20094  plycj  20197  mtest  20322  sqfpc  20922  ostth2lem2  21330  ostth3  21334  lpni  21769  nvz  22160  ubthlem2  22375  chcompl  22747  ocin  22800  hmopidmchi  23656  dmdmd  23805  dmdbr5  23813  mdsl1i  23826  sigaclci  24517  lgamgulmlem1  24815  kur14lem9  24902  sconpht  24918  cvmsdisj  24959  untelirr  25159  untsucf  25161  dedekind  25189  dedekindle  25190  dfon2lem4  25415  dfon2lem6  25417  dfon2lem7  25418  dfon2lem8  25419  dfon2  25421  wfrlem9  25548  frrlem5e  25592  sltval2  25613  refssex  26363  ptfinfin  26380  heibor1lem  26520  heiborlem4  26525  heiborlem6  26527  stoweid  27790  cshwsame  28299  bnj23  29145  atlex  30176  psubspi  30606  elpcliN  30752  ldilval  30972  trlord  31428  tendotp  31620  hdmapval2  32695
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-v 2960
  Copyright terms: Public domain W3C validator