Theorem rspccva 3067

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 3064	. 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 1369   e. wcel 1756   A.wral 2710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2715  df-v 2969

This theorem is referenced by:  disjne  3719  seex  4678  foelrn  5857  fconstfv  5935  grprinvlem  6296  caofid0l  6343  caofid0r  6344  caofid1  6345  caofid2  6346  onnseq  6797  odi  7010  omsmolem  7084  fvixp  7260  unblem1  7556  ordiso2  7721  unwdomg  7791  ac5num  8198  acni2  8208  fodomacn  8218  iundom2g  8696  fpwwe2lem3  8792  eltsk2g  8910  tskpwss  8911  tskpw  8912  tsken  8913  prlem934  9194  dedekindle  9526  ltord1  9858  leord1  9859  eqord1  9860  ltord2  9861  leord2  9862  eqord2  9863  supmul1  10287  seqcaopr2  11834  bccl  12090  hashbc  12198  limsupbnd2  12953  2clim  13042  climsup  13139  caurcvg2  13147  caucvgb  13149  isummulc2  13221  fsumtscopo2  13258  fsumparts  13261  incexclem  13291  isumshft  13294  climcndslem1  13304  climcndslem2  13305  supcvg  13310  geomulcvg  13328  mertenslem2  13337  mertens  13338  rpnnen2lem10  13498  dvdsprime  13768  iscatd2  14611  fuciso  14877  luble  15149  glble  15162  lubub  15281  lubl  15282  mgmlrid  15429  grpinvex  15544  issubg2  15687  issubg4  15691  nmzbi  15712  gagrpid  15803  cntzi  15838  psgnunilem2  15992  sylow1lem3  16090  pgpfi  16095  slwispgp  16101  sylow2alem1  16107  dprdfcl  16487  dprdfclOLD  16493  ablfac2  16580  abveq0  16891  issrngd  16926  psrbagconf1o  17424  pf1ind  17769  phllmhm  18041  ipcl  18042  ipeq0  18047  isphld  18063  ocvi  18074  elcls3  18667  neindisj2  18707  perfi  18739  cnima  18849  1stcfb  19029  1stcelcls  19045  llyi  19058  nllyi  19059  1stckgenlem  19106  ptbasin  19130  txcls  19157  ptcnp  19175  ufli  19467  tgpt0  19669  tsmsxplem2  19708  nrmmetd  20147  tngngp  20220  reperflem  20375  lebnumlem3  20515  htpyi  20526  htpycc  20532  phtpyi  20536  cfili  20759  cmetcvg  20776  caubl  20798  caublcls  20799  bcthlem2  20816  bcthlem3  20817  bcthlem4  20818  ovolicc2lem1  20980  ovolicc2lem5  20984  ovolicc2  20985  voliunlem3  21013  volsuplem  21016  uniioombllem2  21043  mbfima  21090  ismbfd  21098  ismbf3d  21112  mbfmullem  21183  itg2monolem1  21208  itg2i1fseqle  21212  itg2i1fseq  21213  itg2i1fseq2  21214  itg2addlem  21216  bddmulibl  21296  c1liplem1  21448  dvfsumle  21473  dvfsumabs  21475  dvfsumrlimf  21477  dvfsumlem1  21478  dvfsumlem2  21479  dvfsumlem3  21480  dvfsumlem4  21481  dvfsumrlimge0  21482  dvfsum2  21486  ftc1lem6  21493  ulmcau  21840  ulmdvlem1  21845  ulmdvlem3  21847  mtestbdd  21850  itgulm  21853  radcnvlem1  21858  abelthlem5  21880  abelthlem7  21883  areambl  22332  dchrisumlem2  22719  dchrvmasumiflem1  22730  pntpbnd1  22815  ostthlem1  22856  tglowdim1i  22934  brbtwn2  23119  ax5seglem1  23142  ax5seglem2  23143  ax5seglem9  23151  axcontlem4  23181  axcontlem12  23189  usgrcyclnl1  23494  eupaseg  23562  grpoidinvlem3  23661  grpoidinv  23663  grpoidinv2  23673  isgrp2d  23690  cmpidelt  23784  rngoid  23838  vcid  23897  minvecolem5  24250  hcaucvg  24556  hlimconvi  24561  lnopeq0i  25379  cnlnadjlem5  25443  csmdsymi  25706  difelsiga  26545  eulerpartlemb  26720  ballotlemfc0  26844  ballotlemfcc  26845  ptpcon  27091  cvmsdisj  27128  cvmshmeo  27129  snmlflim  27190  sinccvg  27287  preddowncl  27626  bpolycl  28164  bpolydif  28167  mblfinlem1  28399  ovoliunnfl  28404  ex-ovoliunnfl  28405  voliunnfl  28406  volsupnfl  28407  mbfresfi  28409  itg2gt0cn  28418  bddiblnc  28433  ftc1cnnc  28437  ftc1anc  28446  locfinnei  28545  fnemeet1  28558  fnemeet2  28559  fnejoin1  28560  fnejoin2  28561  upixp  28594  filbcmb  28605  sdclem1  28610  seqpo  28614  incsequz2  28616  mettrifi  28624  caushft  28628  sstotbnd2  28644  heibor1lem  28679  heiborlem3  28683  heiborlem10  28690  heibor  28691  rrndstprj2  28701  limsuc2  29364  cncmpmax  29725  climinf  29750  climsuse  29752  stoweidlem7  29773  stoweidlem15  29781  stoweidlem21  29787  stoweidlem31  29797  stoweidlem35  29801  stoweidlem36  29802  stoweidlem50  29816  stoweidlem57  29823  stoweidlem59  29825  wallispilem3  29833  usgreghash2spot  30633  bj-seex  32326