Theorem rspccva 3308

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

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-v 3202

This theorem is referenced by:  disjne  4022  n0snor2el  4364  seex  5077  preddowncl  5707  foelrn  6378  grprinvlem  6872  caofid0l  6925  caofid0r  6926  caofid1  6927  caofid2  6928  onnseq  7441  odi  7659  omsmolem  7733  fvixp  7913  unblem1  8212  ordiso2  8420  unwdomg  8489  ac5num  8859  acni2  8869  fodomacn  8879  iundom2g  9362  fpwwe2lem3  9455  eltsk2g  9573  tskpwss  9574  tskpw  9575  tsken  9576  prlem934  9855  dedekindle  10201  ltord1  10554  leord1  10555  eqord1  10556  ltord2  10557  leord2  10558  eqord2  10559  supmul1  10992  seqcaopr2  12837  bccl  13109  hashbc  13237  limsupbnd2  14214  2clim  14303  climsup  14400  caurcvg2  14408  caucvgb  14410  isummulc2  14493  telfsumo2  14535  fsumparts  14538  incexclem  14568  isumshft  14571  climcndslem1  14581  climcndslem2  14582  supcvg  14588  geomulcvg  14607  mertenslem2  14617  mertens  14618  bpolycl  14783  bpolydif  14786  rpnnen2lem10  14952  dvdsprime  15400  iscatd2  16342  fuciso  16635  luble  16987  glble  17000  lubub  17119  lubl  17120  mgmlrid  17266  grpinvex  17432  issubg2  17609  issubg4  17613  nmzbi  17634  gagrpid  17727  cntzi  17762  psgnunilem2  17915  sylow1lem3  18015  pgpfi  18020  slwispgp  18026  sylow2alem1  18032  dprdfcl  18412  ablfac2  18488  abveq0  18826  issrngd  18861  psrbagconf1o  19374  pf1ind  19719  phllmhm  19977  ipcl  19978  ipeq0  19983  isphld  19999  ocvi  20013  cayhamlem3  20692  elcls3  20887  neindisj2  20927  perfi  20959  cnima  21069  1stcfb  21248  1stcelcls  21264  llyi  21277  nllyi  21278  locfinnei  21326  1stckgenlem  21356  ptbasin  21380  txcls  21407  ptcnp  21425  ufli  21718  tgpt0  21922  tsmsxplem2  21957  nrmmetd  22379  tngngp  22458  tngngp3  22460  reperflem  22621  lebnumlem3  22762  htpyi  22773  htpycc  22779  phtpyi  22783  cfili  23066  cmetcvg  23083  caubl  23106  caublcls  23107  bcthlem2  23122  bcthlem3  23123  bcthlem4  23124  ovolicc2lem1  23285  ovolicc2lem5  23289  ovolicc2  23290  voliunlem3  23320  volsuplem  23323  uniioombllem2  23351  mbfima  23399  ismbfd  23407  ismbf3d  23421  mbfmullem  23492  itg2monolem1  23517  itg2i1fseqle  23521  itg2i1fseq  23522  itg2i1fseq2  23523  itg2addlem  23525  bddmulibl  23605  c1liplem1  23759  dvfsumle  23784  dvfsumabs  23786  dvfsumrlimf  23788  dvfsumlem1  23789  dvfsumlem2  23790  dvfsumlem3  23791  dvfsumlem4  23792  dvfsumrlimge0  23793  dvfsum2  23797  ftc1lem6  23804  ulmcau  24149  ulmdvlem1  24154  ulmdvlem3  24156  mtestbdd  24159  itgulm  24162  radcnvlem1  24167  abelthlem5  24189  abelthlem7  24192  areambl  24685  2lgslem1a  25116  dchrisumlem2  25179  dchrvmasumiflem1  25190  pntpbnd1  25275  ostthlem1  25316  tglowdim1i  25396  brbtwn2  25785  ax5seglem1  25808  ax5seglem2  25809  ax5seglem9  25817  axcontlem4  25847  axcontlem12  25855  0vtxrusgr  26473  fusgreghash2wsp  27202  grpoidinvlem3  27360  grpoidinv  27362  grpoidinv2  27369  vcidOLD  27419  minvecolem5  27737  hcaucvg  28043  hlimconvi  28048  lnopeq0i  28866  cnlnadjlem5  28930  csmdsymi  29193  difelsiga  30196  eulerpartlemb  30430  ballotlemfc0  30554  ballotlemfcc  30555  ptpconn  31215  cvmsdisj  31252  cvmshmeo  31253  snmlflim  31314  elmrsubrn  31417  mvtinf  31452  sinccvg  31567  fnemeet1  32361  fnemeet2  32362  fnejoin1  32363  fnejoin2  32364  bj-seex  32919  poimirlem27  33436  poimirlem32  33441  mblfinlem1  33446  ovoliunnfl  33451  ex-ovoliunnfl  33452  voliunnfl  33453  volsupnfl  33454  mbfresfi  33456  itg2gt0cn  33465  bddiblnc  33480  ftc1cnnc  33484  ftc1anc  33493  upixp  33524  filbcmb  33535  sdclem1  33539  seqpo  33543  incsequz2  33545  mettrifi  33553  caushft  33557  sstotbnd2  33573  heibor1lem  33608  heiborlem3  33612  heiborlem10  33619  heibor  33620  rrndstprj2  33630  cmpidelt  33658  rngoid  33701  limsuc2  37611  cvgdvgrat  38512  cncmpmax  39191  foelrnf  39373  mccllem  39829  mccl  39830  climinf  39838  climsuse  39840  islptre  39851  limcperiod  39860  addlimc  39880  0ellimcdiv  39881  cncficcgt0  40101  fperdvper  40133  dvbdfbdioolem2  40144  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvnprodlem3  40163  stoweidlem7  40224  stoweidlem15  40232  stoweidlem21  40238  stoweidlem31  40248  stoweidlem35  40252  stoweidlem36  40253  stoweidlem50  40267  stoweidlem57  40274  stoweidlem59  40276  wallispilem3  40284  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem32  40356  fourierdlem33  40357  fourierdlem39  40363  fourierdlem62  40385  fourierdlem71  40394  fourierdlem89  40412  fourierdlem91  40414  fourierdlem93  40416  fourierdlem101  40424  fourierdlem103  40426  fourierdlem104  40427  etransclem24  40475  etransclem32  40483  smflimlem6  40984  smfpimcc  41014  smfsuplem2  41018