Theorem rspccva 3193

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 3190	. 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 1381   e. wcel 1802   A.wral 2791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ral 2796  df-v 3095

This theorem is referenced by:  disjne  3854  seex  4828  foelrn  6031  fconstfvOLD  6114  grprinvlem  6494  caofid0l  6549  caofid0r  6550  caofid1  6551  caofid2  6552  onnseq  7013  odi  7226  omsmolem  7300  fvixp  7472  unblem1  7770  ordiso2  7938  unwdomg  8008  ac5num  8415  acni2  8425  fodomacn  8435  iundom2g  8913  fpwwe2lem3  9009  eltsk2g  9127  tskpwss  9128  tskpw  9129  tsken  9130  prlem934  9409  dedekindle  9743  ltord1  10080  leord1  10081  eqord1  10082  ltord2  10083  leord2  10084  eqord2  10085  supmul1  10509  seqcaopr2  12117  bccl  12374  hashbc  12476  limsupbnd2  13280  2clim  13369  climsup  13466  caurcvg2  13474  caucvgb  13476  isummulc2  13551  telfsumo2  13591  fsumparts  13594  incexclem  13622  isumshft  13625  climcndslem1  13635  climcndslem2  13636  supcvg  13641  geomulcvg  13659  mertenslem2  13668  mertens  13669  rpnnen2lem10  13829  dvdsprime  14102  iscatd2  14950  fuciso  15213  luble  15486  glble  15499  lubub  15618  lubl  15619  mgmlrid  15762  grpinvex  15934  issubg2  16085  issubg4  16089  nmzbi  16110  gagrpid  16201  cntzi  16236  psgnunilem2  16389  sylow1lem3  16489  pgpfi  16494  slwispgp  16500  sylow2alem1  16506  dprdfcl  16915  dprdfclOLD  16921  ablfac2  17008  abveq0  17343  issrngd  17378  psrbagconf1o  17894  pf1ind  18259  phllmhm  18534  ipcl  18535  ipeq0  18540  isphld  18556  ocvi  18567  cayhamlem3  19255  elcls3  19450  neindisj2  19490  perfi  19522  cnima  19632  1stcfb  19812  1stcelcls  19828  llyi  19841  nllyi  19842  locfinnei  19890  1stckgenlem  19920  ptbasin  19944  txcls  19971  ptcnp  19989  ufli  20281  tgpt0  20483  tsmsxplem2  20522  nrmmetd  20961  tngngp  21034  reperflem  21189  lebnumlem3  21329  htpyi  21340  htpycc  21346  phtpyi  21350  cfili  21573  cmetcvg  21590  caubl  21612  caublcls  21613  bcthlem2  21630  bcthlem3  21631  bcthlem4  21632  ovolicc2lem1  21794  ovolicc2lem5  21798  ovolicc2  21799  voliunlem3  21828  volsuplem  21831  uniioombllem2  21858  mbfima  21905  ismbfd  21913  ismbf3d  21927  mbfmullem  21998  itg2monolem1  22023  itg2i1fseqle  22027  itg2i1fseq  22028  itg2i1fseq2  22029  itg2addlem  22031  bddmulibl  22111  c1liplem1  22263  dvfsumle  22288  dvfsumabs  22290  dvfsumrlimf  22292  dvfsumlem1  22293  dvfsumlem2  22294  dvfsumlem3  22295  dvfsumlem4  22296  dvfsumrlimge0  22297  dvfsum2  22301  ftc1lem6  22308  ulmcau  22655  ulmdvlem1  22660  ulmdvlem3  22662  mtestbdd  22665  itgulm  22668  radcnvlem1  22673  abelthlem5  22695  abelthlem7  22698  areambl  23153  dchrisumlem2  23540  dchrvmasumiflem1  23551  pntpbnd1  23636  ostthlem1  23677  tglowdim1i  23757  brbtwn2  24073  ax5seglem1  24096  ax5seglem2  24097  ax5seglem9  24105  axcontlem4  24135  axcontlem12  24143  usgrcyclnl1  24505  eupaseg  24838  usgreghash2spot  24934  grpoidinvlem3  25073  grpoidinv  25075  grpoidinv2  25085  isgrp2d  25102  cmpidelt  25196  rngoid  25250  vcid  25309  minvecolem5  25662  hcaucvg  25968  hlimconvi  25973  lnopeq0i  26791  cnlnadjlem5  26855  csmdsymi  27118  difelsiga  27999  eulerpartlemb  28173  ballotlemfc0  28297  ballotlemfcc  28298  ptpcon  28544  cvmsdisj  28581  cvmshmeo  28582  snmlflim  28643  elmrsubrn  28746  mvtinf  28781  sinccvg  28905  preddowncl  29244  bpolycl  29782  bpolydif  29785  mblfinlem1  30019  ovoliunnfl  30024  ex-ovoliunnfl  30025  voliunnfl  30026  volsupnfl  30027  mbfresfi  30029  itg2gt0cn  30038  bddiblnc  30053  ftc1cnnc  30057  ftc1anc  30066  fnemeet1  30152  fnemeet2  30153  fnejoin1  30154  fnejoin2  30155  upixp  30188  filbcmb  30199  sdclem1  30204  seqpo  30208  incsequz2  30210  mettrifi  30218  caushft  30222  sstotbnd2  30238  heibor1lem  30273  heiborlem3  30277  heiborlem10  30284  heibor  30285  rrndstprj2  30295  limsuc2  30954  cvgdvgrat  31163  cncmpmax  31354  climinf  31516  climsuse  31518  islptre  31529  limcperiod  31538  addlimc  31558  0ellimcdiv  31559  cncficcgt0  31594  fperdvper  31615  dvbdfbdioolem2  31626  ioodvbdlimc1lem2  31629  ioodvbdlimc2lem  31631  stoweidlem7  31674  stoweidlem15  31682  stoweidlem21  31688  stoweidlem31  31698  stoweidlem35  31702  stoweidlem36  31703  stoweidlem50  31717  stoweidlem57  31724  stoweidlem59  31726  wallispilem3  31734  dirkercncflem2  31771  dirkercncflem4  31773  fourierdlem32  31806  fourierdlem33  31807  fourierdlem39  31813  fourierdlem62  31836  fourierdlem71  31845  fourierdlem89  31863  fourierdlem91  31865  fourierdlem93  31867  fourierdlem101  31875  fourierdlem103  31877  fourierdlem104  31878  bj-seex  34203