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

Theorem rspccva 2883
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
Hypothesis
Ref Expression
rspcv.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
rspccva  |-  ( ( 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 rspccva
StepHypRef Expression
1 rspcv.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
21rspcv 2880 . 2  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
32impcom 419 1  |-  ( ( A. x  e.  B  ph 
/\  A  e.  B
)  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1623    e. wcel 1684   A.wral 2543
This theorem is referenced by:  disjne  3500  seex  4356  foelrn  5679  fconstfv  5734  grprinvlem  6058  caofid0l  6105  caofid0r  6106  caofid1  6107  caofid2  6108  onnseq  6361  odi  6577  omsmolem  6651  fvixp  6821  unblem1  7109  ordiso2  7230  ac5num  7663  acni2  7673  fodomacn  7683  iundom2g  8162  fpwwe2lem3  8255  eltsk2g  8373  tskpwss  8374  tskpw  8375  tsken  8376  prlem934  8657  ltord1  9299  leord1  9300  eqord1  9301  ltord2  9302  leord2  9303  eqord2  9304  supmul1  9719  seqcaopr2  11082  bccl  11334  hashbc  11391  limsupbnd2  11957  2clim  12046  climsup  12143  caurcvg2  12150  caucvgb  12152  isummulc2  12225  fsumtscopo2  12261  fsumparts  12264  incexclem  12295  isumshft  12298  climcndslem1  12308  climcndslem2  12309  supcvg  12314  geomulcvg  12332  mertenslem2  12341  mertens  12342  rpnnen2lem10  12502  dvdsprime  12771  iscatd2  13583  fuciso  13849  lubub  14223  lubl  14224  mgmlrid  14389  grpinvex  14497  issubg2  14636  issubg4  14638  nmzbi  14657  gagrpid  14748  cntzi  14805  sylow1lem3  14911  pgpfi  14916  slwispgp  14922  sylow2alem1  14928  dprdfcl  15248  ablfac2  15324  abveq0  15591  issrngd  15626  psrbagconf1o  16120  phllmhm  16536  ipcl  16537  ipeq0  16542  isphld  16558  ocvi  16569  elcls3  16820  neindisj2  16860  perfi  16886  cnima  16994  1stcfb  17171  1stcelcls  17187  llyi  17200  nllyi  17201  1stckgenlem  17248  ptbasin  17272  txcls  17299  ptcnp  17316  ufli  17609  tgpt0  17801  tsmsxplem2  17836  nrmmetd  18097  tngngp  18170  reperflem  18323  lebnumlem3  18461  htpyi  18472  htpycc  18478  phtpyi  18482  cfili  18694  cmetcvg  18711  caubl  18733  caublcls  18734  bcthlem2  18747  bcthlem3  18748  bcthlem4  18749  ovolicc2lem1  18876  ovolicc2lem5  18880  ovolicc2  18881  voliunlem3  18909  volsuplem  18912  uniioombllem2  18938  mbfima  18987  ismbfd  18995  ismbf3d  19009  mbfmullem  19080  itg2monolem1  19105  itg2i1fseqle  19109  itg2i1fseq  19110  itg2i1fseq2  19111  itg2addlem  19113  bddmulibl  19193  c1liplem1  19343  dvfsumle  19368  dvfsumabs  19370  dvfsumrlimf  19372  dvfsumlem1  19373  dvfsumlem2  19374  dvfsumlem3  19375  dvfsumlem4  19376  dvfsumrlimge0  19377  dvfsum2  19381  ftc1lem6  19388  pf1ind  19438  ulmcau  19772  ulmdvlem1  19777  ulmdvlem3  19779  itgulm  19784  radcnvlem1  19789  abelthlem5  19811  abelthlem7  19814  areambl  20253  dchrisumlem2  20639  dchrvmasumiflem1  20650  pntpbnd1  20735  ostthlem1  20776  grpoidinvlem3  20873  grpoidinv  20875  grpoidinv2  20885  isgrp2d  20902  cmpidelt  20996  rngoid  21050  vcid  21107  minvecolem5  21460  hcaucvg  21765  hlimconvi  21770  lnopeq0i  22587  cnlnadjlem5  22651  csmdsymi  22914  ballotlemfc0  23051  ballotlemfcc  23052  difelsiga  23494  ptpcon  23764  cvmsdisj  23801  cvmshmeo  23802  eupaseg  23888  snmlflim  23915  sinccvg  24006  dedekindle  24083  preddowncl  24196  brbtwn2  24533  ax5seglem1  24556  ax5seglem2  24557  ax5seglem9  24565  axcontlem4  24595  axcontlem12  24603  bpolycl  24787  bpolydif  24790  bclelnu  25155  pfsubkl  26047  pgapspf2  26053  locfinnei  26302  fnemeet1  26315  fnemeet2  26316  fnejoin1  26317  fnejoin2  26318  upixp  26403  filbcmb  26432  sdclem1  26453  seqpo  26457  incsequz2  26459  mettrifi  26473  caushft  26477  sstotbnd2  26498  heibor1lem  26533  heiborlem3  26537  heiborlem10  26544  heibor  26545  rrndstprj2  26555  limsuc2  27137  psgnunilem2  27418  cncmpmax  27703  climinf  27732  climsuse  27734  stoweidlem7  27756  stoweidlem15  27764  stoweidlem21  27770  stoweidlem31  27780  stoweidlem35  27784  stoweidlem36  27785  stoweidlem50  27799  stoweidlem57  27806  stoweidlem59  27808  wallispilem3  27816
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-v 2790
  Copyright terms: Public domain W3C validator