Theorem rspccva 3061

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

Step	Hyp	Ref	Expression
1		rspcv.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
2	1	rspcv 3058	. 2 |- ( A e. B -> ( A. x e. B ph -> ps ) )
3	2	impcom 430	1 |- ( ( A. x e. B ph /\ A e. B ) -> ps )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = 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:  disjne  3712  seex  4670  foelrn  5850  fconstfv  5927  grprinvlem  6290  caofid0l  6337  caofid0r  6338  caofid1  6339  caofid2  6340  onnseq  6791  odi  7006  omsmolem  7080  fvixp  7256  unblem1  7552  ordiso2  7717  unwdomg  7787  ac5num  8194  acni2  8204  fodomacn  8214  iundom2g  8692  fpwwe2lem3  8787  eltsk2g  8905  tskpwss  8906  tskpw  8907  tsken  8908  prlem934  9189  dedekindle  9521  ltord1  9853  leord1  9854  eqord1  9855  ltord2  9856  leord2  9857  eqord2  9858  supmul1  10282  seqcaopr2  11825  bccl  12081  hashbc  12189  limsupbnd2  12944  2clim  13033  climsup  13130  caurcvg2  13138  caucvgb  13140  isummulc2  13212  fsumtscopo2  13248  fsumparts  13251  incexclem  13281  isumshft  13284  climcndslem1  13294  climcndslem2  13295  supcvg  13300  geomulcvg  13318  mertenslem2  13327  mertens  13328  rpnnen2lem10  13488  dvdsprime  13758  iscatd2  14601  fuciso  14867  luble  15139  glble  15152  lubub  15271  lubl  15272  mgmlrid  15419  grpinvex  15532  issubg2  15675  issubg4  15679  nmzbi  15700  gagrpid  15791  cntzi  15826  psgnunilem2  15980  sylow1lem3  16078  pgpfi  16083  slwispgp  16089  sylow2alem1  16095  dprdfcl  16470  dprdfclOLD  16476  ablfac2  16563  abveq0  16834  issrngd  16869  psrbagconf1o  17377  phllmhm  17902  ipcl  17903  ipeq0  17908  isphld  17924  ocvi  17935  elcls3  18528  neindisj2  18568  perfi  18600  cnima  18710  1stcfb  18890  1stcelcls  18906  llyi  18919  nllyi  18920  1stckgenlem  18967  ptbasin  18991  txcls  19018  ptcnp  19036  ufli  19328  tgpt0  19530  tsmsxplem2  19569  nrmmetd  20008  tngngp  20081  reperflem  20236  lebnumlem3  20376  htpyi  20387  htpycc  20393  phtpyi  20397  cfili  20620  cmetcvg  20637  caubl  20659  caublcls  20660  bcthlem2  20677  bcthlem3  20678  bcthlem4  20679  ovolicc2lem1  20841  ovolicc2lem5  20845  ovolicc2  20846  voliunlem3  20874  volsuplem  20877  uniioombllem2  20904  mbfima  20951  ismbfd  20959  ismbf3d  20973  mbfmullem  21044  itg2monolem1  21069  itg2i1fseqle  21073  itg2i1fseq  21074  itg2i1fseq2  21075  itg2addlem  21077  bddmulibl  21157  c1liplem1  21309  dvfsumle  21334  dvfsumabs  21336  dvfsumrlimf  21338  dvfsumlem1  21339  dvfsumlem2  21340  dvfsumlem3  21341  dvfsumlem4  21342  dvfsumrlimge0  21343  dvfsum2  21347  ftc1lem6  21354  pf1ind  21405  ulmcau  21744  ulmdvlem1  21749  ulmdvlem3  21751  mtestbdd  21754  itgulm  21757  radcnvlem1  21762  abelthlem5  21784  abelthlem7  21787  areambl  22236  dchrisumlem2  22623  dchrvmasumiflem1  22634  pntpbnd1  22719  ostthlem1  22760  tglowdim1i  22835  brbtwn2  22973  ax5seglem1  22996  ax5seglem2  22997  ax5seglem9  23005  axcontlem4  23035  axcontlem12  23043  usgrcyclnl1  23348  eupaseg  23416  grpoidinvlem3  23515  grpoidinv  23517  grpoidinv2  23527  isgrp2d  23544  cmpidelt  23638  rngoid  23692  vcid  23751  minvecolem5  24104  hcaucvg  24410  hlimconvi  24415  lnopeq0i  25233  cnlnadjlem5  25297  csmdsymi  25560  difelsiga  26429  eulerpartlemb  26598  ballotlemfc0  26722  ballotlemfcc  26723  ptpcon  26969  cvmsdisj  27006  cvmshmeo  27007  snmlflim  27068  sinccvg  27164  preddowncl  27503  bpolycl  28041  bpolydif  28044  mblfinlem1  28269  ovoliunnfl  28274  ex-ovoliunnfl  28275  voliunnfl  28276  volsupnfl  28277  mbfresfi  28279  itg2gt0cn  28288  bddiblnc  28303  ftc1cnnc  28307  ftc1anc  28316  locfinnei  28415  fnemeet1  28428  fnemeet2  28429  fnejoin1  28430  fnejoin2  28431  upixp  28464  filbcmb  28475  sdclem1  28480  seqpo  28484  incsequz2  28486  mettrifi  28494  caushft  28498  sstotbnd2  28514  heibor1lem  28549  heiborlem3  28553  heiborlem10  28560  heibor  28561  rrndstprj2  28571  limsuc2  29235  cncmpmax  29596  climinf  29622  climsuse  29624  stoweidlem7  29645  stoweidlem15  29653  stoweidlem21  29659  stoweidlem31  29669  stoweidlem35  29673  stoweidlem36  29674  stoweidlem50  29688  stoweidlem57  29695  stoweidlem59  29697  wallispilem3  29705  usgreghash2spot  30505  bj-seex  32010