Theorem rspccva 3580

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	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
rspccva	⊢ ((∀𝑥 ∈ 𝐵 𝜑 ∧ 𝐴 ∈ 𝐵) → 𝜓)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspccva

Step	Hyp	Ref	Expression
1		rspcv.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
2	1	rspcv 3577	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
3	2	impcom 411	1 ⊢ ((∀𝑥 ∈ 𝐵 𝜑 ∧ 𝐴 ∈ 𝐵) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1560   ∈ wcel 2142  ∀wral 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077

This theorem is referenced by:  disjne  4409  n0snor2el  4791  seex  5606  preddowncl  6319  frpoins3g  6333  foelrn  7088  foelrnf  7089  caofid0l  7693  caofid0r  7694  caofid1  7695  caofid2  7696  onnseq  8315  odi  8548  omsmolem  8627  naddssim  8656  fvixp  8884  unblem1  9236  ordiso2  9463  unwdomg  9532  ac5num  9992  acni2  10002  fodomacn  10012  iundom2g  10497  fpwwe2lem3  10591  eltsk2g  10709  tskpwss  10710  tskpw  10711  tsken  10712  prlem934  10991  dedekindle  11347  ltord1  11713  leord1  11714  eqord1  11715  ltord2  11716  leord2  11717  eqord2  11718  supmul1  12161  seqcaopr2  14051  bccl  14335  hashbc  14466  limsupbnd2  15510  2clim  15599  climsup  15697  caurcvg2  15705  caucvgb  15707  isummulc2  15789  telfsumo2  15831  fsumparts  15834  incexclem  15866  isumshft  15869  climcndslem1  15879  climcndslem2  15880  supcvg  15886  geomulcvg  15906  mertenslem2  15915  mertens  15916  bpolycl  16082  bpolydif  16085  rpnnen2lem10  16255  dvdsprime  16721  fuciso  18011  lubub  18543  lubl  18544  mgmlrid  18701  grpinvalem  18707  grpinvex  18985  issubg2  19183  issubg4  19187  nmzbi  19205  gagrpid  19334  cntzi  19369  psgnunilem2  19535  sylow1lem3  19640  pgpfi  19645  slwispgp  19651  sylow2alem1  19657  dprdfcl  20055  ablfac2  20131  abveq0  20867  issrngd  20904  phllmhm  21684  ipcl  21685  ipeq0  21690  isphld  21706  ocvi  21721  pf1ind  22418  cayhamlem3  22947  elcls3  23143  neindisj2  23183  perfi  23215  cnima  23325  1stcfb  23505  1stcelcls  23521  llyi  23534  nllyi  23535  locfinnei  23583  1stckgenlem  23613  ptbasin  23637  txcls  23664  ptcnp  23682  ufli  23974  tgpt0  24179  tsmsxplem2  24214  nrmmetd  24634  tngngp  24714  tngngp3  24716  reperflem  24879  lebnumlem3  25025  htpyi  25036  htpycc  25042  phtpyi  25046  cfili  25330  cmetcvg  25347  caubl  25370  caublcls  25371  bcthlem2  25387  bcthlem3  25388  bcthlem4  25389  ovolicc2lem1  25579  ovolicc2lem5  25583  ovolicc2  25584  voliunlem3  25614  volsuplem  25617  uniioombllem2  25645  mbfima  25692  ismbfd  25701  ismbf3d  25716  mbfmullem  25787  itg2monolem1  25812  itg2i1fseqle  25816  itg2i1fseq  25817  itg2i1fseq2  25818  itg2addlem  25820  bddmulibl  25901  bddiblnc  25904  c1liplem1  26058  dvfsumle  26083  dvfsumabs  26085  dvfsumrlimf  26087  dvfsumlem1  26088  dvfsumlem2  26089  dvfsumlem3  26090  dvfsumlem4  26091  dvfsumrlimge0  26092  dvfsum2  26096  ftc1lem6  26103  ulmcau  26458  ulmdvlem1  26463  ulmdvlem3  26465  mtestbdd  26468  itgulm  26471  radcnvlem1  26476  abelthlem5  26498  abelthlem7  26501  areambl  27023  2lgslem1a  27455  dchrisumlem2  27554  dchrvmasumiflem1  27565  pntpbnd1  27650  ostthlem1  27691  madebday  27993  addscom  28059  precsexlem9  28308  peano5n0s  28412  bdayfinbndlem1  28560  tglowdim1i  28670  brbtwn2  29106  ax5seglem1  29129  ax5seglem2  29130  ax5seglem9  29138  axcontlem4  29168  axcontlem12  29176  fusgreghash2wsp  30540  grpoidinvlem3  30709  grpoidinv  30711  grpoidinv2  30718  vcidOLD  30767  minvecolem5  31084  hcaucvg  31389  hlimconvi  31394  lnopeq0i  32210  cnlnadjlem5  32274  csmdsymi  32537  difelsiga  34430  eulerpartlemb  34665  ballotlemfc0  34790  ballotlemfcc  34791  ptpconn  35583  cvmsdisj  35620  cvmshmeo  35621  snmlflim  35682  elmrsubrn  35870  mvtinf  35905  sinccvg  36023  nmulprop  36540  fnemeet1  36726  fnemeet2  36727  fnejoin1  36728  fnejoin2  36729  bj-seex  37407  poimirlem27  38146  poimirlem32  38151  mblfinlem1  38156  ovoliunnfl  38161  ex-ovoliunnfl  38162  voliunnfl  38163  volsupnfl  38164  mbfresfi  38165  itg2gt0cn  38174  ftc1cnnc  38191  ftc1anc  38200  upixp  38228  filbcmb  38239  sdclem1  38242  seqpo  38246  incsequz2  38248  mettrifi  38256  caushft  38260  sstotbnd2  38273  heibor1lem  38308  heiborlem3  38312  heiborlem10  38319  heibor  38320  rrndstprj2  38330  cmpidelt  38358  rngoid  38401  fsuppind  43172  limsuc2  43618  cvgdvgrat  44889  cncmpmax  45612  mccllem  46173  mccl  46174  climinf  46182  climsuse  46184  islptre  46195  limcperiod  46204  addlimc  46222  0ellimcdiv  46223  cncficcgt0  46462  dvbdfbdioolem2  46503  ioodvbdlimc1lem2  46506  ioodvbdlimc2lem  46508  dvnprodlem3  46522  stoweidlem7  46581  stoweidlem15  46589  stoweidlem21  46595  stoweidlem31  46605  stoweidlem35  46609  stoweidlem36  46610  stoweidlem50  46624  stoweidlem57  46631  stoweidlem59  46633  wallispilem3  46641  dirkercncflem2  46678  dirkercncflem4  46680  fourierdlem32  46713  fourierdlem33  46714  fourierdlem39  46720  fourierdlem62  46742  fourierdlem71  46751  fourierdlem89  46769  fourierdlem91  46771  fourierdlem93  46773  fourierdlem101  46781  fourierdlem103  46783  fourierdlem104  46784  etransclem24  46832  etransclem32  46840  smflimlem6  47350  smfpimcc  47382  smfsuplem2  47386  gricushgr  48539