Theorem rspccva 3149

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 3146	. 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 1444   e. wcel 1887   A.wral 2737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ral 2742  df-v 3047

This theorem is referenced by:  disjne  3810  seex  4797  preddowncl  5407  foelrn  6041  fconstfvOLD  6127  grprinvlem  6507  caofid0l  6559  caofid0r  6560  caofid1  6561  caofid2  6562  onnseq  7063  odi  7280  omsmolem  7354  fvixp  7527  unblem1  7823  ordiso2  8030  unwdomg  8099  ac5num  8467  acni2  8477  fodomacn  8487  iundom2g  8965  fpwwe2lem3  9058  eltsk2g  9176  tskpwss  9177  tskpw  9178  tsken  9179  prlem934  9458  dedekindle  9798  ltord1  10140  leord1  10141  eqord1  10142  ltord2  10143  leord2  10144  eqord2  10145  supmul1  10576  seqcaopr2  12249  bccl  12507  hashbc  12616  limsupbnd2  13546  limsupbnd2OLD  13547  2clim  13636  climsup  13733  caurcvg2  13744  caucvgb  13746  isummulc2  13823  telfsumo2  13863  fsumparts  13866  incexclem  13894  isumshft  13897  climcndslem1  13907  climcndslem2  13908  supcvg  13914  geomulcvg  13932  mertenslem2  13941  mertens  13942  bpolycl  14105  bpolydif  14108  rpnnen2lem10  14276  dvdsprime  14637  iscatd2  15587  fuciso  15880  luble  16233  glble  16246  lubub  16365  lubl  16366  mgmlrid  16509  grpinvex  16681  issubg2  16832  issubg4  16836  nmzbi  16857  gagrpid  16948  cntzi  16983  psgnunilem2  17136  sylow1lem3  17252  pgpfi  17257  slwispgp  17263  sylow2alem1  17269  dprdfcl  17646  ablfac2  17722  abveq0  18054  issrngd  18089  psrbagconf1o  18598  pf1ind  18943  phllmhm  19199  ipcl  19200  ipeq0  19205  isphld  19221  ocvi  19232  cayhamlem3  19911  elcls3  20099  neindisj2  20139  perfi  20171  cnima  20281  1stcfb  20460  1stcelcls  20476  llyi  20489  nllyi  20490  locfinnei  20538  1stckgenlem  20568  ptbasin  20592  txcls  20619  ptcnp  20637  ufli  20929  tgpt0  21133  tsmsxplem2  21168  nrmmetd  21589  tngngp  21662  reperflem  21836  lebnumlem3  21991  lebnumlem3OLD  21994  htpyi  22005  htpycc  22011  phtpyi  22015  cfili  22238  cmetcvg  22255  caubl  22277  caublcls  22278  bcthlem2  22293  bcthlem3  22294  bcthlem4  22295  ovolicc2lem1  22470  ovolicc2lem5  22475  ovolicc2  22476  voliunlem3  22505  volsuplem  22508  uniioombllem2  22540  uniioombllem2OLD  22541  mbfima  22588  ismbfd  22596  ismbf3d  22610  mbfmullem  22683  itg2monolem1  22708  itg2i1fseqle  22712  itg2i1fseq  22713  itg2i1fseq2  22714  itg2addlem  22716  bddmulibl  22796  c1liplem1  22948  dvfsumle  22973  dvfsumabs  22975  dvfsumrlimf  22977  dvfsumlem1  22978  dvfsumlem2  22979  dvfsumlem3  22980  dvfsumlem4  22981  dvfsumrlimge0  22982  dvfsum2  22986  ftc1lem6  22993  ulmcau  23350  ulmdvlem1  23355  ulmdvlem3  23357  mtestbdd  23360  itgulm  23363  radcnvlem1  23368  abelthlem5  23390  abelthlem7  23393  areambl  23884  dchrisumlem2  24328  dchrvmasumiflem1  24339  pntpbnd1  24424  ostthlem1  24465  tglowdim1i  24545  brbtwn2  24935  ax5seglem1  24958  ax5seglem2  24959  ax5seglem9  24967  axcontlem4  24997  axcontlem12  25005  usgrcyclnl1  25368  eupaseg  25701  usgreghash2spot  25797  grpoidinvlem3  25934  grpoidinv  25936  grpoidinv2  25946  isgrp2d  25963  cmpidelt  26057  rngoid  26111  vcid  26170  minvecolem5  26523  minvecolem5OLD  26533  hcaucvg  26839  hlimconvi  26844  lnopeq0i  27660  cnlnadjlem5  27724  csmdsymi  27987  difelsiga  28955  eulerpartlemb  29201  ballotlemfc0  29325  ballotlemfcc  29326  ptpcon  29956  cvmsdisj  29993  cvmshmeo  29994  snmlflim  30055  elmrsubrn  30158  mvtinf  30193  sinccvg  30317  fnemeet1  31022  fnemeet2  31023  fnejoin1  31024  fnejoin2  31025  bj-seex  31526  poimirlem27  31967  poimirlem32  31972  mblfinlem1  31977  ovoliunnfl  31982  ex-ovoliunnfl  31983  voliunnfl  31984  volsupnfl  31985  mbfresfi  31987  itg2gt0cn  31997  bddiblnc  32012  ftc1cnnc  32016  ftc1anc  32025  upixp  32056  filbcmb  32067  sdclem1  32072  seqpo  32076  incsequz2  32078  mettrifi  32086  caushft  32090  sstotbnd2  32106  heibor1lem  32141  heiborlem3  32145  heiborlem10  32152  heibor  32153  rrndstprj2  32163  limsuc2  35899  cvgdvgrat  36662  cncmpmax  37353  foelrnf  37461  mccllem  37677  mccl  37678  climinf  37684  climinfOLD  37685  climsuse  37687  islptre  37699  limcperiod  37708  addlimc  37729  0ellimcdiv  37730  cncficcgt0  37766  fperdvper  37790  dvbdfbdioolem2  37801  ioodvbdlimc1lem2  37804  ioodvbdlimc1lem2OLD  37806  ioodvbdlimc2lem  37808  ioodvbdlimc2lemOLD  37809  dvnprodlem3  37823  stoweidlem7  37867  stoweidlem15  37875  stoweidlem21  37881  stoweidlem31  37892  stoweidlem35  37896  stoweidlem36  37897  stoweidlem50  37911  stoweidlem57  37918  stoweidlem59  37920  wallispilem3  37929  dirkercncflem2  37966  dirkercncflem4  37968  fourierdlem32  38002  fourierdlem33  38003  fourierdlem39  38009  fourierdlem62  38032  fourierdlem71  38041  fourierdlem89  38059  fourierdlem91  38061  fourierdlem93  38063  fourierdlem101  38071  fourierdlem103  38073  fourierdlem104  38074  etransclem24  38123  etransclem32  38131  0vtxrusgr  39593