Theorem rspccva 3559

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 3556	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
3	2	impcom 408	1 ⊢ ((∀𝑥 ∈ 𝐵 𝜑 ∧ 𝐴 ∈ 𝐵) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054

This theorem is referenced by:  disjne  4383  n0snor2el  4764  seex  5577  preddowncl  6283  frpoins3g  6297  foelrn  7048  foelrnf  7049  caofid0l  7653  caofid0r  7654  caofid1  7655  caofid2  7656  onnseq  8274  odi  8504  omsmolem  8583  naddssim  8611  fvixp  8840  unblem1  9192  ordiso2  9420  unwdomg  9489  ac5num  9949  acni2  9959  fodomacn  9969  iundom2g  10453  fpwwe2lem3  10547  eltsk2g  10665  tskpwss  10666  tskpw  10667  tsken  10668  prlem934  10947  dedekindle  11301  ltord1  11667  leord1  11668  eqord1  11669  ltord2  11670  leord2  11671  eqord2  11672  supmul1  12116  seqcaopr2  13991  bccl  14275  hashbc  14406  limsupbnd2  15436  2clim  15525  climsup  15623  caurcvg2  15631  caucvgb  15633  isummulc2  15715  telfsumo2  15757  fsumparts  15760  incexclem  15792  isumshft  15795  climcndslem1  15805  climcndslem2  15806  supcvg  15812  geomulcvg  15832  mertenslem2  15841  mertens  15842  bpolycl  16008  bpolydif  16011  rpnnen2lem10  16181  dvdsprime  16647  fuciso  17936  lubub  18468  lubl  18469  mgmlrid  18626  grpinvalem  18632  grpinvex  18910  issubg2  19108  issubg4  19112  nmzbi  19130  gagrpid  19260  cntzi  19295  psgnunilem2  19461  sylow1lem3  19566  pgpfi  19571  slwispgp  19577  sylow2alem1  19583  dprdfcl  19981  ablfac2  20057  abveq0  20790  issrngd  20827  phllmhm  21607  ipcl  21608  ipeq0  21613  isphld  21629  ocvi  21644  pf1ind  22341  cayhamlem3  22870  elcls3  23066  neindisj2  23106  perfi  23138  cnima  23248  1stcfb  23428  1stcelcls  23444  llyi  23457  nllyi  23458  locfinnei  23506  1stckgenlem  23536  ptbasin  23560  txcls  23587  ptcnp  23605  ufli  23897  tgpt0  24102  tsmsxplem2  24137  nrmmetd  24557  tngngp  24637  tngngp3  24639  reperflem  24802  lebnumlem3  24948  htpyi  24959  htpycc  24965  phtpyi  24969  cfili  25253  cmetcvg  25270  caubl  25293  caublcls  25294  bcthlem2  25310  bcthlem3  25311  bcthlem4  25312  ovolicc2lem1  25502  ovolicc2lem5  25506  ovolicc2  25507  voliunlem3  25537  volsuplem  25540  uniioombllem2  25568  mbfima  25615  ismbfd  25624  ismbf3d  25639  mbfmullem  25710  itg2monolem1  25735  itg2i1fseqle  25739  itg2i1fseq  25740  itg2i1fseq2  25741  itg2addlem  25743  bddmulibl  25824  bddiblnc  25827  c1liplem1  25981  dvfsumle  26006  dvfsumabs  26008  dvfsumrlimf  26010  dvfsumlem1  26011  dvfsumlem2  26012  dvfsumlem3  26013  dvfsumlem4  26014  dvfsumrlimge0  26015  dvfsum2  26019  ftc1lem6  26026  ulmcau  26378  ulmdvlem1  26383  ulmdvlem3  26385  mtestbdd  26388  itgulm  26391  radcnvlem1  26396  abelthlem5  26418  abelthlem7  26421  areambl  26940  2lgslem1a  27372  dchrisumlem2  27471  dchrvmasumiflem1  27482  pntpbnd1  27567  ostthlem1  27608  madebday  27910  addscom  27976  precsexlem9  28225  peano5n0s  28329  bdayfinbndlem1  28477  tglowdim1i  28587  brbtwn2  28992  ax5seglem1  29015  ax5seglem2  29016  ax5seglem9  29024  axcontlem4  29054  axcontlem12  29062  fusgreghash2wsp  30426  grpoidinvlem3  30595  grpoidinv  30597  grpoidinv2  30604  vcidOLD  30653  minvecolem5  30970  hcaucvg  31275  hlimconvi  31280  lnopeq0i  32096  cnlnadjlem5  32160  csmdsymi  32423  difelsiga  34317  eulerpartlemb  34552  ballotlemfc0  34677  ballotlemfcc  34678  ptpconn  35461  cvmsdisj  35498  cvmshmeo  35499  snmlflim  35560  elmrsubrn  35748  mvtinf  35783  sinccvg  35901  fnemeet1  36594  fnemeet2  36595  fnejoin1  36596  fnejoin2  36597  bj-seex  37275  poimirlem27  38014  poimirlem32  38019  mblfinlem1  38024  ovoliunnfl  38029  ex-ovoliunnfl  38030  voliunnfl  38031  volsupnfl  38032  mbfresfi  38033  itg2gt0cn  38042  ftc1cnnc  38059  ftc1anc  38068  upixp  38096  filbcmb  38107  sdclem1  38110  seqpo  38114  incsequz2  38116  mettrifi  38124  caushft  38128  sstotbnd2  38141  heibor1lem  38176  heiborlem3  38180  heiborlem10  38187  heibor  38188  rrndstprj2  38198  cmpidelt  38226  rngoid  38269  fsuppind  43040  limsuc2  43486  cvgdvgrat  44757  cncmpmax  45480  mccllem  46042  mccl  46043  climinf  46051  climsuse  46053  islptre  46064  limcperiod  46073  addlimc  46091  0ellimcdiv  46092  cncficcgt0  46331  dvbdfbdioolem2  46372  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  dvnprodlem3  46391  stoweidlem7  46450  stoweidlem15  46458  stoweidlem21  46464  stoweidlem31  46474  stoweidlem35  46478  stoweidlem36  46479  stoweidlem50  46493  stoweidlem57  46500  stoweidlem59  46502  wallispilem3  46510  dirkercncflem2  46547  dirkercncflem4  46549  fourierdlem32  46582  fourierdlem33  46583  fourierdlem39  46589  fourierdlem62  46611  fourierdlem71  46620  fourierdlem89  46638  fourierdlem91  46640  fourierdlem93  46642  fourierdlem101  46650  fourierdlem103  46652  fourierdlem104  46653  etransclem24  46701  etransclem32  46709  smflimlem6  47219  smfpimcc  47251  smfsuplem2  47255  gricushgr  48408