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

Theorem rspccva 2896
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 2893 . 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 1632    e. wcel 1696   A.wral 2556
This theorem is referenced by:  disjne  3513  seex  4372  foelrn  5695  fconstfv  5750  grprinvlem  6074  caofid0l  6121  caofid0r  6122  caofid1  6123  caofid2  6124  onnseq  6377  odi  6593  omsmolem  6667  fvixp  6837  unblem1  7125  ordiso2  7246  ac5num  7679  acni2  7689  fodomacn  7699  iundom2g  8178  fpwwe2lem3  8271  eltsk2g  8389  tskpwss  8390  tskpw  8391  tsken  8392  prlem934  8673  ltord1  9315  leord1  9316  eqord1  9317  ltord2  9318  leord2  9319  eqord2  9320  supmul1  9735  seqcaopr2  11098  bccl  11350  hashbc  11407  limsupbnd2  11973  2clim  12062  climsup  12159  caurcvg2  12166  caucvgb  12168  isummulc2  12241  fsumtscopo2  12277  fsumparts  12280  incexclem  12311  isumshft  12314  climcndslem1  12324  climcndslem2  12325  supcvg  12330  geomulcvg  12348  mertenslem2  12357  mertens  12358  rpnnen2lem10  12518  dvdsprime  12787  iscatd2  13599  fuciso  13865  lubub  14239  lubl  14240  mgmlrid  14405  grpinvex  14513  issubg2  14652  issubg4  14654  nmzbi  14673  gagrpid  14764  cntzi  14821  sylow1lem3  14927  pgpfi  14932  slwispgp  14938  sylow2alem1  14944  dprdfcl  15264  ablfac2  15340  abveq0  15607  issrngd  15642  psrbagconf1o  16136  phllmhm  16552  ipcl  16553  ipeq0  16558  isphld  16574  ocvi  16585  elcls3  16836  neindisj2  16876  perfi  16902  cnima  17010  1stcfb  17187  1stcelcls  17203  llyi  17216  nllyi  17217  1stckgenlem  17264  ptbasin  17288  txcls  17315  ptcnp  17332  ufli  17625  tgpt0  17817  tsmsxplem2  17852  nrmmetd  18113  tngngp  18186  reperflem  18339  lebnumlem3  18477  htpyi  18488  htpycc  18494  phtpyi  18498  cfili  18710  cmetcvg  18727  caubl  18749  caublcls  18750  bcthlem2  18763  bcthlem3  18764  bcthlem4  18765  ovolicc2lem1  18892  ovolicc2lem5  18896  ovolicc2  18897  voliunlem3  18925  volsuplem  18928  uniioombllem2  18954  mbfima  19003  ismbfd  19011  ismbf3d  19025  mbfmullem  19096  itg2monolem1  19121  itg2i1fseqle  19125  itg2i1fseq  19126  itg2i1fseq2  19127  itg2addlem  19129  bddmulibl  19209  c1liplem1  19359  dvfsumle  19384  dvfsumabs  19386  dvfsumrlimf  19388  dvfsumlem1  19389  dvfsumlem2  19390  dvfsumlem3  19391  dvfsumlem4  19392  dvfsumrlimge0  19393  dvfsum2  19397  ftc1lem6  19404  pf1ind  19454  ulmcau  19788  ulmdvlem1  19793  ulmdvlem3  19795  itgulm  19800  radcnvlem1  19805  abelthlem5  19827  abelthlem7  19830  areambl  20269  dchrisumlem2  20655  dchrvmasumiflem1  20666  pntpbnd1  20751  ostthlem1  20792  grpoidinvlem3  20889  grpoidinv  20891  grpoidinv2  20901  isgrp2d  20918  cmpidelt  21012  rngoid  21066  vcid  21123  minvecolem5  21476  hcaucvg  21781  hlimconvi  21786  lnopeq0i  22603  cnlnadjlem5  22667  csmdsymi  22930  ballotlemfc0  23067  ballotlemfcc  23068  difelsiga  23509  ptpcon  23779  cvmsdisj  23816  cvmshmeo  23817  eupaseg  23903  snmlflim  23930  sinccvg  24021  dedekindle  24098  preddowncl  24267  brbtwn2  24605  ax5seglem1  24628  ax5seglem2  24629  ax5seglem9  24637  axcontlem4  24667  axcontlem12  24675  bpolycl  24859  bpolydif  24862  ovoliunnfl  25001  ex-ovoliunnfl  25002  itg2gt0cn  25006  bddiblnc  25021  ftc1cnnc  25025  bclelnu  25258  pfsubkl  26150  pgapspf2  26156  locfinnei  26405  fnemeet1  26418  fnemeet2  26419  fnejoin1  26420  fnejoin2  26421  upixp  26506  filbcmb  26535  sdclem1  26556  seqpo  26560  incsequz2  26562  mettrifi  26576  caushft  26580  sstotbnd2  26601  heibor1lem  26636  heiborlem3  26640  heiborlem10  26647  heibor  26648  rrndstprj2  26658  limsuc2  27240  psgnunilem2  27521  cncmpmax  27806  climinf  27835  climsuse  27837  stoweidlem7  27859  stoweidlem15  27867  stoweidlem21  27873  stoweidlem31  27883  stoweidlem35  27887  stoweidlem36  27888  stoweidlem50  27902  stoweidlem57  27909  stoweidlem59  27911  wallispilem3  27919
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