Theorem rspccva 3584

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045

This theorem is referenced by:  disjne  4414  n0snor2el  4793  seex  5590  preddowncl  6293  frpoins3g  6307  foelrn  7061  foelrnf  7062  caofid0l  7666  caofid0r  7667  caofid1  7668  caofid2  7669  onnseq  8290  odi  8520  omsmolem  8598  naddssim  8626  fvixp  8852  unblem1  9215  ordiso2  9444  unwdomg  9513  ac5num  9965  acni2  9975  fodomacn  9985  iundom2g  10469  fpwwe2lem3  10562  eltsk2g  10680  tskpwss  10681  tskpw  10682  tsken  10683  prlem934  10962  dedekindle  11314  ltord1  11680  leord1  11681  eqord1  11682  ltord2  11683  leord2  11684  eqord2  11685  supmul1  12128  seqcaopr2  13979  bccl  14263  hashbc  14394  limsupbnd2  15425  2clim  15514  climsup  15612  caurcvg2  15620  caucvgb  15622  isummulc2  15704  telfsumo2  15745  fsumparts  15748  incexclem  15778  isumshft  15781  climcndslem1  15791  climcndslem2  15792  supcvg  15798  geomulcvg  15818  mertenslem2  15827  mertens  15828  bpolycl  15994  bpolydif  15997  rpnnen2lem10  16167  dvdsprime  16633  fuciso  17916  lubub  18446  lubl  18447  mgmlrid  18570  grpinvalem  18576  grpinvex  18851  issubg2  19049  issubg4  19053  nmzbi  19072  gagrpid  19202  cntzi  19237  psgnunilem2  19401  sylow1lem3  19506  pgpfi  19511  slwispgp  19517  sylow2alem1  19523  dprdfcl  19921  ablfac2  19997  abveq0  20703  issrngd  20740  phllmhm  21517  ipcl  21518  ipeq0  21523  isphld  21539  ocvi  21554  pf1ind  22218  cayhamlem3  22750  elcls3  22946  neindisj2  22986  perfi  23018  cnima  23128  1stcfb  23308  1stcelcls  23324  llyi  23337  nllyi  23338  locfinnei  23386  1stckgenlem  23416  ptbasin  23440  txcls  23467  ptcnp  23485  ufli  23777  tgpt0  23982  tsmsxplem2  24017  nrmmetd  24438  tngngp  24518  tngngp3  24520  reperflem  24683  lebnumlem3  24838  htpyi  24849  htpycc  24855  phtpyi  24859  cfili  25144  cmetcvg  25161  caubl  25184  caublcls  25185  bcthlem2  25201  bcthlem3  25202  bcthlem4  25203  ovolicc2lem1  25394  ovolicc2lem5  25398  ovolicc2  25399  voliunlem3  25429  volsuplem  25432  uniioombllem2  25460  mbfima  25507  ismbfd  25516  ismbf3d  25531  mbfmullem  25602  itg2monolem1  25627  itg2i1fseqle  25631  itg2i1fseq  25632  itg2i1fseq2  25633  itg2addlem  25635  bddmulibl  25716  bddiblnc  25719  c1liplem1  25877  dvfsumle  25902  dvfsumleOLD  25903  dvfsumabs  25905  dvfsumrlimf  25907  dvfsumlem1  25908  dvfsumlem2  25909  dvfsumlem2OLD  25910  dvfsumlem3  25911  dvfsumlem4  25912  dvfsumrlimge0  25913  dvfsum2  25917  ftc1lem6  25924  ulmcau  26280  ulmdvlem1  26285  ulmdvlem3  26287  mtestbdd  26290  itgulm  26293  radcnvlem1  26298  abelthlem5  26321  abelthlem7  26324  areambl  26844  2lgslem1a  27278  dchrisumlem2  27377  dchrvmasumiflem1  27388  pntpbnd1  27473  ostthlem1  27514  madebday  27787  addscom  27849  precsexlem9  28093  peano5n0s  28188  zs12bday  28319  tglowdim1i  28404  brbtwn2  28808  ax5seglem1  28831  ax5seglem2  28832  ax5seglem9  28840  axcontlem4  28870  axcontlem12  28878  fusgreghash2wsp  30240  grpoidinvlem3  30408  grpoidinv  30410  grpoidinv2  30417  vcidOLD  30466  minvecolem5  30783  hcaucvg  31088  hlimconvi  31093  lnopeq0i  31909  cnlnadjlem5  31973  csmdsymi  32236  difelsiga  34096  eulerpartlemb  34332  ballotlemfc0  34457  ballotlemfcc  34458  ptpconn  35193  cvmsdisj  35230  cvmshmeo  35231  snmlflim  35292  elmrsubrn  35480  mvtinf  35515  sinccvg  35633  fnemeet1  36327  fnemeet2  36328  fnejoin1  36329  fnejoin2  36330  bj-seex  36883  poimirlem27  37614  poimirlem32  37619  mblfinlem1  37624  ovoliunnfl  37629  ex-ovoliunnfl  37630  voliunnfl  37631  volsupnfl  37632  mbfresfi  37633  itg2gt0cn  37642  ftc1cnnc  37659  ftc1anc  37668  upixp  37696  filbcmb  37707  sdclem1  37710  seqpo  37714  incsequz2  37716  mettrifi  37724  caushft  37728  sstotbnd2  37741  heibor1lem  37776  heiborlem3  37780  heiborlem10  37787  heibor  37788  rrndstprj2  37798  cmpidelt  37826  rngoid  37869  fsuppind  42551  limsuc2  43003  cvgdvgrat  44275  cncmpmax  44999  mccllem  45568  mccl  45569  climinf  45577  climsuse  45579  islptre  45590  limcperiod  45599  addlimc  45619  0ellimcdiv  45620  cncficcgt0  45859  dvbdfbdioolem2  45900  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  dvnprodlem3  45919  stoweidlem7  45978  stoweidlem15  45986  stoweidlem21  45992  stoweidlem31  46002  stoweidlem35  46006  stoweidlem36  46007  stoweidlem50  46021  stoweidlem57  46028  stoweidlem59  46030  wallispilem3  46038  dirkercncflem2  46075  dirkercncflem4  46077  fourierdlem32  46110  fourierdlem33  46111  fourierdlem39  46117  fourierdlem62  46139  fourierdlem71  46148  fourierdlem89  46166  fourierdlem91  46168  fourierdlem93  46170  fourierdlem101  46178  fourierdlem103  46180  fourierdlem104  46181  etransclem24  46229  etransclem32  46237  smflimlem6  46747  smfpimcc  46779  smfsuplem2  46783  gricushgr  47890