Theorem rspccva 3182

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 3179	. 2 |- ( A e. B -> ( A. x e. B ph -> ps ) )
3	2	impcom 432	1 |- ( ( A. x e. B ph /\ A e. B ) -> ps )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   = wceq 1438   e. wcel 1869   A.wral 2776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ral 2781  df-v 3084

This theorem is referenced by:  disjne  3839  seex  4814  preddowncl  5424  foelrn  6054  fconstfvOLD  6140  grprinvlem  6519  caofid0l  6571  caofid0r  6572  caofid1  6573  caofid2  6574  onnseq  7069  odi  7286  omsmolem  7360  fvixp  7533  unblem1  7827  ordiso2  8034  unwdomg  8103  ac5num  8469  acni2  8479  fodomacn  8489  iundom2g  8967  fpwwe2lem3  9060  eltsk2g  9178  tskpwss  9179  tskpw  9180  tsken  9181  prlem934  9460  dedekindle  9800  ltord1  10142  leord1  10143  eqord1  10144  ltord2  10145  leord2  10146  eqord2  10147  supmul1  10578  seqcaopr2  12250  bccl  12508  hashbc  12615  limsupbnd2  13539  limsupbnd2OLD  13540  2clim  13629  climsup  13726  caurcvg2  13737  caucvgb  13739  isummulc2  13816  telfsumo2  13856  fsumparts  13859  incexclem  13887  isumshft  13890  climcndslem1  13900  climcndslem2  13901  supcvg  13907  geomulcvg  13925  mertenslem2  13934  mertens  13935  bpolycl  14098  bpolydif  14101  rpnnen2lem10  14269  dvdsprime  14630  iscatd2  15580  fuciso  15873  luble  16226  glble  16239  lubub  16358  lubl  16359  mgmlrid  16502  grpinvex  16674  issubg2  16825  issubg4  16829  nmzbi  16850  gagrpid  16941  cntzi  16976  psgnunilem2  17129  sylow1lem3  17245  pgpfi  17250  slwispgp  17256  sylow2alem1  17262  dprdfcl  17639  ablfac2  17715  abveq0  18047  issrngd  18082  psrbagconf1o  18591  pf1ind  18936  phllmhm  19191  ipcl  19192  ipeq0  19197  isphld  19213  ocvi  19224  cayhamlem3  19903  elcls3  20091  neindisj2  20131  perfi  20163  cnima  20273  1stcfb  20452  1stcelcls  20468  llyi  20481  nllyi  20482  locfinnei  20530  1stckgenlem  20560  ptbasin  20584  txcls  20611  ptcnp  20629  ufli  20921  tgpt0  21125  tsmsxplem2  21160  nrmmetd  21581  tngngp  21654  reperflem  21828  lebnumlem3  21983  lebnumlem3OLD  21986  htpyi  21997  htpycc  22003  phtpyi  22007  cfili  22230  cmetcvg  22247  caubl  22269  caublcls  22270  bcthlem2  22285  bcthlem3  22286  bcthlem4  22287  ovolicc2lem1  22462  ovolicc2lem5  22467  ovolicc2  22468  voliunlem3  22497  volsuplem  22500  uniioombllem2  22532  uniioombllem2OLD  22533  mbfima  22580  ismbfd  22588  ismbf3d  22602  mbfmullem  22675  itg2monolem1  22700  itg2i1fseqle  22704  itg2i1fseq  22705  itg2i1fseq2  22706  itg2addlem  22708  bddmulibl  22788  c1liplem1  22940  dvfsumle  22965  dvfsumabs  22967  dvfsumrlimf  22969  dvfsumlem1  22970  dvfsumlem2  22971  dvfsumlem3  22972  dvfsumlem4  22973  dvfsumrlimge0  22974  dvfsum2  22978  ftc1lem6  22985  ulmcau  23342  ulmdvlem1  23347  ulmdvlem3  23349  mtestbdd  23352  itgulm  23355  radcnvlem1  23360  abelthlem5  23382  abelthlem7  23385  areambl  23876  dchrisumlem2  24320  dchrvmasumiflem1  24331  pntpbnd1  24416  ostthlem1  24457  tglowdim1i  24537  brbtwn2  24927  ax5seglem1  24950  ax5seglem2  24951  ax5seglem9  24959  axcontlem4  24989  axcontlem12  24997  usgrcyclnl1  25360  eupaseg  25693  usgreghash2spot  25789  grpoidinvlem3  25926  grpoidinv  25928  grpoidinv2  25938  isgrp2d  25955  cmpidelt  26049  rngoid  26103  vcid  26162  minvecolem5  26515  minvecolem5OLD  26525  hcaucvg  26831  hlimconvi  26836  lnopeq0i  27652  cnlnadjlem5  27716  csmdsymi  27979  difelsiga  28957  eulerpartlemb  29203  ballotlemfc0  29327  ballotlemfcc  29328  ptpcon  29958  cvmsdisj  29995  cvmshmeo  29996  snmlflim  30057  elmrsubrn  30160  mvtinf  30195  sinccvg  30319  fnemeet1  31021  fnemeet2  31022  fnejoin1  31023  fnejoin2  31024  bj-seex  31489  poimirlem27  31925  poimirlem32  31930  mblfinlem1  31935  ovoliunnfl  31940  ex-ovoliunnfl  31941  voliunnfl  31942  volsupnfl  31943  mbfresfi  31945  itg2gt0cn  31955  bddiblnc  31970  ftc1cnnc  31974  ftc1anc  31983  upixp  32014  filbcmb  32025  sdclem1  32030  seqpo  32034  incsequz2  32036  mettrifi  32044  caushft  32048  sstotbnd2  32064  heibor1lem  32099  heiborlem3  32103  heiborlem10  32110  heibor  32111  rrndstprj2  32121  limsuc2  35863  cvgdvgrat  36564  cncmpmax  37258  foelrnf  37355  mccllem  37541  mccl  37542  climinf  37548  climinfOLD  37549  climsuse  37551  islptre  37563  limcperiod  37572  addlimc  37593  0ellimcdiv  37594  cncficcgt0  37630  fperdvper  37654  dvbdfbdioolem2  37665  ioodvbdlimc1lem2  37668  ioodvbdlimc1lem2OLD  37670  ioodvbdlimc2lem  37672  ioodvbdlimc2lemOLD  37673  dvnprodlem3  37687  stoweidlem7  37731  stoweidlem15  37739  stoweidlem21  37745  stoweidlem31  37756  stoweidlem35  37760  stoweidlem36  37761  stoweidlem50  37775  stoweidlem57  37782  stoweidlem59  37784  wallispilem3  37793  dirkercncflem2  37830  dirkercncflem4  37832  fourierdlem32  37866  fourierdlem33  37867  fourierdlem39  37873  fourierdlem62  37896  fourierdlem71  37905  fourierdlem89  37923  fourierdlem91  37925  fourierdlem93  37927  fourierdlem101  37935  fourierdlem103  37937  fourierdlem104  37938  etransclem24  37987  etransclem32  37995