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

Theorem rspccva 3206
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 3203 . 2  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
32impcom 428 1  |-  ( ( A. x  e.  B  ph 
/\  A  e.  B
)  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1398    e. wcel 1823   A.wral 2804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-v 3108
This theorem is referenced by:  disjne  3860  seex  4831  foelrn  6026  fconstfvOLD  6109  grprinvlem  6486  caofid0l  6541  caofid0r  6542  caofid1  6543  caofid2  6544  onnseq  7007  odi  7220  omsmolem  7294  fvixp  7467  unblem1  7764  ordiso2  7932  unwdomg  8002  ac5num  8408  acni2  8418  fodomacn  8428  iundom2g  8906  fpwwe2lem3  9000  eltsk2g  9118  tskpwss  9119  tskpw  9120  tsken  9121  prlem934  9400  dedekindle  9734  ltord1  10075  leord1  10076  eqord1  10077  ltord2  10078  leord2  10079  eqord2  10080  supmul1  10503  seqcaopr2  12125  bccl  12382  hashbc  12486  limsupbnd2  13388  2clim  13477  climsup  13574  caurcvg2  13582  caucvgb  13584  isummulc2  13659  telfsumo2  13699  fsumparts  13702  incexclem  13730  isumshft  13733  climcndslem1  13743  climcndslem2  13744  supcvg  13749  geomulcvg  13767  mertenslem2  13776  mertens  13777  rpnnen2lem10  14041  dvdsprime  14314  iscatd2  15170  fuciso  15463  luble  15816  glble  15829  lubub  15948  lubl  15949  mgmlrid  16092  grpinvex  16264  issubg2  16415  issubg4  16419  nmzbi  16440  gagrpid  16531  cntzi  16566  psgnunilem2  16719  sylow1lem3  16819  pgpfi  16824  slwispgp  16830  sylow2alem1  16836  dprdfcl  17242  dprdfclOLD  17248  ablfac2  17335  abveq0  17670  issrngd  17705  psrbagconf1o  18221  pf1ind  18586  phllmhm  18840  ipcl  18841  ipeq0  18846  isphld  18862  ocvi  18873  cayhamlem3  19555  elcls3  19751  neindisj2  19791  perfi  19823  cnima  19933  1stcfb  20112  1stcelcls  20128  llyi  20141  nllyi  20142  locfinnei  20190  1stckgenlem  20220  ptbasin  20244  txcls  20271  ptcnp  20289  ufli  20581  tgpt0  20783  tsmsxplem2  20822  nrmmetd  21261  tngngp  21334  reperflem  21489  lebnumlem3  21629  htpyi  21640  htpycc  21646  phtpyi  21650  cfili  21873  cmetcvg  21890  caubl  21912  caublcls  21913  bcthlem2  21930  bcthlem3  21931  bcthlem4  21932  ovolicc2lem1  22094  ovolicc2lem5  22098  ovolicc2  22099  voliunlem3  22128  volsuplem  22131  uniioombllem2  22158  mbfima  22205  ismbfd  22213  ismbf3d  22227  mbfmullem  22298  itg2monolem1  22323  itg2i1fseqle  22327  itg2i1fseq  22328  itg2i1fseq2  22329  itg2addlem  22331  bddmulibl  22411  c1liplem1  22563  dvfsumle  22588  dvfsumabs  22590  dvfsumrlimf  22592  dvfsumlem1  22593  dvfsumlem2  22594  dvfsumlem3  22595  dvfsumlem4  22596  dvfsumrlimge0  22597  dvfsum2  22601  ftc1lem6  22608  ulmcau  22956  ulmdvlem1  22961  ulmdvlem3  22963  mtestbdd  22966  itgulm  22969  radcnvlem1  22974  abelthlem5  22996  abelthlem7  22999  areambl  23486  dchrisumlem2  23873  dchrvmasumiflem1  23884  pntpbnd1  23969  ostthlem1  24010  tglowdim1i  24093  brbtwn2  24410  ax5seglem1  24433  ax5seglem2  24434  ax5seglem9  24442  axcontlem4  24472  axcontlem12  24480  usgrcyclnl1  24842  eupaseg  25175  usgreghash2spot  25271  grpoidinvlem3  25406  grpoidinv  25408  grpoidinv2  25418  isgrp2d  25435  cmpidelt  25529  rngoid  25583  vcid  25642  minvecolem5  25995  hcaucvg  26301  hlimconvi  26306  lnopeq0i  27124  cnlnadjlem5  27188  csmdsymi  27451  difelsiga  28363  eulerpartlemb  28571  ballotlemfc0  28695  ballotlemfcc  28696  ptpcon  28942  cvmsdisj  28979  cvmshmeo  28980  snmlflim  29041  elmrsubrn  29144  mvtinf  29179  sinccvg  29303  preddowncl  29516  bpolycl  30042  bpolydif  30045  mblfinlem1  30291  ovoliunnfl  30296  ex-ovoliunnfl  30297  voliunnfl  30298  volsupnfl  30299  mbfresfi  30301  itg2gt0cn  30310  bddiblnc  30325  ftc1cnnc  30329  ftc1anc  30338  fnemeet1  30424  fnemeet2  30425  fnejoin1  30426  fnejoin2  30427  upixp  30460  filbcmb  30471  sdclem1  30476  seqpo  30480  incsequz2  30482  mettrifi  30490  caushft  30494  sstotbnd2  30510  heibor1lem  30545  heiborlem3  30549  heiborlem10  30556  heibor  30557  rrndstprj2  30567  limsuc2  31225  cvgdvgrat  31435  cncmpmax  31647  mccllem  31844  mccl  31845  climinf  31851  climsuse  31853  islptre  31864  limcperiod  31873  addlimc  31893  0ellimcdiv  31894  cncficcgt0  31930  fperdvper  31954  dvbdfbdioolem2  31965  ioodvbdlimc1lem2  31968  ioodvbdlimc2lem  31970  dvnprodlem3  31984  stoweidlem7  32028  stoweidlem15  32036  stoweidlem21  32042  stoweidlem31  32052  stoweidlem35  32056  stoweidlem36  32057  stoweidlem50  32071  stoweidlem57  32078  stoweidlem59  32080  wallispilem3  32088  dirkercncflem2  32125  dirkercncflem4  32127  fourierdlem32  32160  fourierdlem33  32161  fourierdlem39  32167  fourierdlem62  32190  fourierdlem71  32199  fourierdlem89  32217  fourierdlem91  32219  fourierdlem93  32221  fourierdlem101  32229  fourierdlem103  32231  fourierdlem104  32232  etransclem24  32280  etransclem32  32288  bj-seex  34892
  Copyright terms: Public domain W3C validator