Theorem rspcva 3307

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-2005.)

Hypothesis

Ref	Expression
rspcv.1	|- ( x = A -> ( ph <-> ps ) )

Assertion

Ref	Expression
rspcva	|- ( ( A e. B /\ A. x e. B ph ) -> ps )

Distinct variable groups:   x, A   x, B   ps, x

Allowed substitution hint:   ph( x)

Proof of Theorem rspcva

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	imp 445	1 |- ( ( A e. B /\ A. x e. B ph ) -> 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:  rexraleqim  3328  fvn0ssdmfun  6350  fveqdmss  6354  fvcofneq  6367  caofinvl  6924  tfisi  7058  suppssov1  7327  wfr3g  7413  wfrlem17  7431  tfrlem1  7472  boxriin  7950  boxcutc  7951  marypha1lem  8339  marypha1  8340  supmo  8358  infmo  8401  wemaplem2  8452  unwdomg  8489  isinffi  8818  dfac9  8958  sornom  9099  fin23lem11  9139  fin1a2lem13  9234  axdc3lem2  9273  winalim2  9518  grothac  9652  nqereu  9751  nnsub  11059  zextle  11450  xrsupsslem  12137  xrinfmsslem  12138  supxrunb1  12149  supxrunb2  12150  injresinjlem  12588  ssnn0fi  12784  suppssfz  12794  faclbnd4lem4  13083  ishashinf  13247  rexuz3  14088  cau3lem  14094  caubnd2  14097  o1co  14317  climcn1  14322  incexclem  14568  dvdsext  15043  cshwsidrepsw  15800  prdsbasprj  16132  mreintcl  16255  isacs2  16314  acsfiel  16315  initoeu1  16661  initoeu2  16666  termoeu1  16668  isdrs2  16939  lublecllem  16988  joinle  17014  meetle  17028  acsdrsel  17167  isacs4lem  17168  isacs5lem  17169  acsdrscl  17170  acsficl  17171  mgmidmo  17259  gsumval2  17280  mrcmndind  17366  dfgrp3lem  17513  symgfix2  17836  odeq  17969  gexid  17996  mplind  19502  gsummoncoe1  19674  psgndiflemB  19946  m2detleiblem3  20435  m2detleiblem4  20436  cpmatmcllem  20523  mp2pm2mplem4  20614  cayleyhamilton1  20697  cmpsublem  21202  cmpsub  21203  hauscmplem  21209  cmpfii  21212  ptpjcn  21414  isufil2  21712  ufileu  21723  isucn2  22083  cfiluweak  22099  lpbl  22308  lmmbr  23056  caussi  23095  mdeglt  23825  deg1lt  23857  ply1divex  23896  plyco0  23948  dgrco  24031  emcllem7  24728  isppw2  24841  pntleme  25297  pntlemp  25299  tglowdim2ln  25546  uvtxanbgrvtx  26293  rusgrnumwwlks  26869  clwwlksf  26915  eupthseg  27066  upgreupthseg  27069  vdgn1frgrv2  27160  frgrregorufr  27189  extwwlkfablem1  27207  grpoidinvlem3  27360  grpoideu  27363  lnconi  28892  fsumiunle  29575  rngurd  29788  tpr2rico  29958  esumiun  30156  ofcfeqd2  30163  0elsiga  30177  sigaclci  30195  dya2icoseg2  30340  signstfvneq0  30649  derangsn  31152  frr3g  31779  fwddifnp1  32272  poimirlem25  33434  poimirlem26  33435  poimirlem30  33439  poimirlem31  33440  poimirlem32  33441  heicant  33444  mblfinlem2  33447  ftc1anc  33493  fdc  33541  bndss  33585  isdrngo2  33757  divrngidl  33827  maxidlmax  33842  cdleme0nex  35577  dihglblem2N  36583  hgmapvs  37183  ismrcd1  37261  nacsfg  37268  isnacs3  37273  nacsfix  37275  mzpcl1  37292  mzpcl2  37293  mzpcong  37539  dnnumch1  37614  fnwe2lem2  37621  aomclem1  37624  aomclem4  37627  aomclem6  37629  lnr2i  37686  hbtlem5  37698  hbt  37700  pwssfi  39211  eliind  39240  rexanuz3  39275  choicefi  39392  fsneq  39398  rnmptbd2lem  39463  rnmptbdlem  39470  suplesup  39555  xralrple2  39570  infxr  39583  infleinf  39588  xralrple4  39589  xralrple3  39590  xrralrecnnge  39613  supxrunb3  39623  supxrleubrnmpt  39632  unb2ltle  39642  suprleubrnmpt  39649  infxrgelbrnmpt  39683  supminfxr  39694  islpcn  39871  limclner  39883  climd  39904  clim2d  39905  limsupmnflem  39952  limsupre3uzlem  39967  liminflelimsuplem  40007  xlimxrre  40057  xlimmnfvlem1  40058  xlimmnfv  40060  xlimpnfvlem1  40062  xlimpnfv  40064  climxlim2lem  40071  cncfshift  40087  cncfperiod  40092  ioodvbdlimc1lem1  40146  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  fourierdlem103  40426  fourierdlem104  40427  etransclem48  40499  salunicl  40536  saluncl  40537  subsaliuncllem  40575  sge0pnffigt  40613  meadjuni  40674  omessle  40712  caragensplit  40714  omeunile  40719  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvle  40814  vonvolmbllem  40874  vonvolmbl  40875  pimdecfgtioc  40925  smfpreimalt  40940  smfpreimaltf  40945  smfpreimale  40963  smfpreimagt  40970  smfpreimage  40990  smfmullem4  41001  smfinflem  41023  iccpartimp  41353  iccpartrn  41366  iccpartiun  41370  icceuelpart  41372  reuccatpfxs1  41434  lidldomn1  41921  ply1mulgsumlem2  42175  lindslinindsimp2lem5  42251  lindslinindsimp2  42252  snlindsntor  42260  nn0sumshdiglemA  42413  nn0sumshdiglemB  42414  nn0sumshdig  42417