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

Step	Hyp	Ref	Expression
1		rspcv.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
2	1	rspcv 3203	. 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 1374   e. wcel 1762   A.wral 2807

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ral 2812  df-v 3108

This theorem is referenced by:  disjne  3865  seex  4835  foelrn  6031  fconstfv  6114  grprinvlem  6488  caofid0l  6543  caofid0r  6544  caofid1  6545  caofid2  6546  onnseq  7005  odi  7218  omsmolem  7292  fvixp  7464  unblem1  7761  ordiso2  7929  unwdomg  7999  ac5num  8406  acni2  8416  fodomacn  8426  iundom2g  8904  fpwwe2lem3  9000  eltsk2g  9118  tskpwss  9119  tskpw  9120  tsken  9121  prlem934  9400  dedekindle  9733  ltord1  10068  leord1  10069  eqord1  10070  ltord2  10071  leord2  10072  eqord2  10073  supmul1  10497  seqcaopr2  12099  bccl  12355  hashbc  12455  limsupbnd2  13255  2clim  13344  climsup  13441  caurcvg2  13449  caucvgb  13451  isummulc2  13526  telfsumo2  13566  fsumparts  13569  incexclem  13600  isumshft  13603  climcndslem1  13613  climcndslem2  13614  supcvg  13619  geomulcvg  13637  mertenslem2  13646  mertens  13647  rpnnen2lem10  13807  dvdsprime  14078  iscatd2  14925  fuciso  15191  luble  15463  glble  15476  lubub  15595  lubl  15596  mgmlrid  15743  grpinvex  15859  issubg2  16004  issubg4  16008  nmzbi  16029  gagrpid  16120  cntzi  16155  psgnunilem2  16309  sylow1lem3  16409  pgpfi  16414  slwispgp  16420  sylow2alem1  16426  dprdfcl  16830  dprdfclOLD  16836  ablfac2  16923  abveq0  17251  issrngd  17286  psrbagconf1o  17790  pf1ind  18155  phllmhm  18427  ipcl  18428  ipeq0  18433  isphld  18449  ocvi  18460  cayhamlem3  19148  elcls3  19343  neindisj2  19383  perfi  19415  cnima  19525  1stcfb  19705  1stcelcls  19721  llyi  19734  nllyi  19735  1stckgenlem  19782  ptbasin  19806  txcls  19833  ptcnp  19851  ufli  20143  tgpt0  20345  tsmsxplem2  20384  nrmmetd  20823  tngngp  20896  reperflem  21051  lebnumlem3  21191  htpyi  21202  htpycc  21208  phtpyi  21212  cfili  21435  cmetcvg  21452  caubl  21474  caublcls  21475  bcthlem2  21492  bcthlem3  21493  bcthlem4  21494  ovolicc2lem1  21656  ovolicc2lem5  21660  ovolicc2  21661  voliunlem3  21690  volsuplem  21693  uniioombllem2  21720  mbfima  21767  ismbfd  21775  ismbf3d  21789  mbfmullem  21860  itg2monolem1  21885  itg2i1fseqle  21889  itg2i1fseq  21890  itg2i1fseq2  21891  itg2addlem  21893  bddmulibl  21973  c1liplem1  22125  dvfsumle  22150  dvfsumabs  22152  dvfsumrlimf  22154  dvfsumlem1  22155  dvfsumlem2  22156  dvfsumlem3  22157  dvfsumlem4  22158  dvfsumrlimge0  22159  dvfsum2  22163  ftc1lem6  22170  ulmcau  22517  ulmdvlem1  22522  ulmdvlem3  22524  mtestbdd  22527  itgulm  22530  radcnvlem1  22535  abelthlem5  22557  abelthlem7  22560  areambl  23009  dchrisumlem2  23396  dchrvmasumiflem1  23407  pntpbnd1  23492  ostthlem1  23533  tglowdim1i  23613  brbtwn2  23877  ax5seglem1  23900  ax5seglem2  23901  ax5seglem9  23909  axcontlem4  23939  axcontlem12  23947  usgrcyclnl1  24302  eupaseg  24635  grpoidinvlem3  24734  grpoidinv  24736  grpoidinv2  24746  isgrp2d  24763  cmpidelt  24857  rngoid  24911  vcid  24970  minvecolem5  25323  hcaucvg  25629  hlimconvi  25634  lnopeq0i  26452  cnlnadjlem5  26516  csmdsymi  26779  difelsiga  27623  eulerpartlemb  27797  ballotlemfc0  27921  ballotlemfcc  27922  ptpcon  28168  cvmsdisj  28205  cvmshmeo  28206  snmlflim  28267  sinccvg  28364  preddowncl  28703  bpolycl  29241  bpolydif  29244  mblfinlem1  29479  ovoliunnfl  29484  ex-ovoliunnfl  29485  voliunnfl  29486  volsupnfl  29487  mbfresfi  29489  itg2gt0cn  29498  bddiblnc  29513  ftc1cnnc  29517  ftc1anc  29526  locfinnei  29625  fnemeet1  29638  fnemeet2  29639  fnejoin1  29640  fnejoin2  29641  upixp  29674  filbcmb  29685  sdclem1  29690  seqpo  29694  incsequz2  29696  mettrifi  29704  caushft  29708  sstotbnd2  29724  heibor1lem  29759  heiborlem3  29763  heiborlem10  29770  heibor  29771  rrndstprj2  29781  limsuc2  30443  cncmpmax  30804  climinf  30967  climsuse  30969  islptre  30980  limcperiod  30989  addlimc  31009  0ellimcdiv  31010  cncficcgt0  31046  fperdvper  31067  dvbdfbdioolem2  31078  ioodvbdlimc1lem2  31081  ioodvbdlimc2lem  31083  stoweidlem7  31126  stoweidlem15  31134  stoweidlem21  31140  stoweidlem31  31150  stoweidlem35  31154  stoweidlem36  31155  stoweidlem50  31169  stoweidlem57  31176  stoweidlem59  31178  wallispilem3  31186  dirkercncflem2  31223  dirkercncflem4  31225  fourierdlem32  31258  fourierdlem33  31259  fourierdlem39  31265  fourierdlem62  31288  fourierdlem71  31297  fourierdlem89  31315  fourierdlem91  31317  fourierdlem93  31319  fourierdlem101  31327  fourierdlem103  31329  fourierdlem104  31330  usgreghash2spot  31788  bj-seex  33447