Theorem rspccva 3581

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∀wral 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061

This theorem is referenced by:  disjne  4419  n0snor2el  4796  seex  5600  preddowncl  6291  frpoins3g  6305  foelrn  7061  caofid0l  7653  caofid0r  7654  caofid1  7655  caofid2  7656  onnseq  8295  odi  8531  omsmolem  8608  naddssim  8636  fvixp  8847  unblem1  9246  ordiso2  9460  unwdomg  9529  ac5num  9981  acni2  9991  fodomacn  10001  iundom2g  10485  fpwwe2lem3  10578  eltsk2g  10696  tskpwss  10697  tskpw  10698  tsken  10699  prlem934  10978  dedekindle  11328  ltord1  11690  leord1  11691  eqord1  11692  ltord2  11693  leord2  11694  eqord2  11695  supmul1  12133  seqcaopr2  13954  bccl  14232  hashbc  14362  limsupbnd2  15377  2clim  15466  climsup  15566  caurcvg2  15574  caucvgb  15576  isummulc2  15658  telfsumo2  15699  fsumparts  15702  incexclem  15732  isumshft  15735  climcndslem1  15745  climcndslem2  15746  supcvg  15752  geomulcvg  15772  mertenslem2  15781  mertens  15782  bpolycl  15946  bpolydif  15949  rpnnen2lem10  16116  dvdsprime  16574  fuciso  17878  lubub  18414  lubl  18415  mgmlrid  18536  grprinvlem  18542  grpinvex  18772  issubg2  18957  issubg4  18961  nmzbi  18980  gagrpid  19088  cntzi  19123  psgnunilem2  19291  sylow1lem3  19396  pgpfi  19401  slwispgp  19407  sylow2alem1  19413  dprdfcl  19806  ablfac2  19882  abveq0  20341  issrngd  20376  phllmhm  21073  ipcl  21074  ipeq0  21079  isphld  21095  ocvi  21110  psrbagconf1oOLD  21376  pf1ind  21758  cayhamlem3  22273  elcls3  22471  neindisj2  22511  perfi  22543  cnima  22653  1stcfb  22833  1stcelcls  22849  llyi  22862  nllyi  22863  locfinnei  22911  1stckgenlem  22941  ptbasin  22965  txcls  22992  ptcnp  23010  ufli  23302  tgpt0  23507  tsmsxplem2  23542  nrmmetd  23967  tngngp  24055  tngngp3  24057  reperflem  24218  lebnumlem3  24363  htpyi  24374  htpycc  24380  phtpyi  24384  cfili  24669  cmetcvg  24686  caubl  24709  caublcls  24710  bcthlem2  24726  bcthlem3  24727  bcthlem4  24728  ovolicc2lem1  24918  ovolicc2lem5  24922  ovolicc2  24923  voliunlem3  24953  volsuplem  24956  uniioombllem2  24984  mbfima  25031  ismbfd  25040  ismbf3d  25055  mbfmullem  25127  itg2monolem1  25152  itg2i1fseqle  25156  itg2i1fseq  25157  itg2i1fseq2  25158  itg2addlem  25160  bddmulibl  25240  bddiblnc  25243  c1liplem1  25397  dvfsumle  25422  dvfsumabs  25424  dvfsumrlimf  25426  dvfsumlem1  25427  dvfsumlem2  25428  dvfsumlem3  25429  dvfsumlem4  25430  dvfsumrlimge0  25431  dvfsum2  25435  ftc1lem6  25442  ulmcau  25791  ulmdvlem1  25796  ulmdvlem3  25798  mtestbdd  25801  itgulm  25804  radcnvlem1  25809  abelthlem5  25831  abelthlem7  25834  areambl  26345  2lgslem1a  26776  dchrisumlem2  26875  dchrvmasumiflem1  26886  pntpbnd1  26971  ostthlem1  27012  madebday  27272  addscom  27321  tglowdim1i  27506  brbtwn2  27917  ax5seglem1  27940  ax5seglem2  27941  ax5seglem9  27949  axcontlem4  27979  axcontlem12  27987  fusgreghash2wsp  29345  grpoidinvlem3  29511  grpoidinv  29513  grpoidinv2  29520  vcidOLD  29569  minvecolem5  29886  hcaucvg  30191  hlimconvi  30196  lnopeq0i  31012  cnlnadjlem5  31076  csmdsymi  31339  difelsiga  32821  eulerpartlemb  33057  ballotlemfc0  33181  ballotlemfcc  33182  ptpconn  33914  cvmsdisj  33951  cvmshmeo  33952  snmlflim  34013  elmrsubrn  34201  mvtinf  34236  sinccvg  34348  fnemeet1  34914  fnemeet2  34915  fnejoin1  34916  fnejoin2  34917  bj-seex  35465  poimirlem27  36178  poimirlem32  36183  mblfinlem1  36188  ovoliunnfl  36193  ex-ovoliunnfl  36194  voliunnfl  36195  volsupnfl  36196  mbfresfi  36197  itg2gt0cn  36206  ftc1cnnc  36223  ftc1anc  36232  upixp  36261  filbcmb  36272  sdclem1  36275  seqpo  36279  incsequz2  36281  mettrifi  36289  caushft  36293  sstotbnd2  36306  heibor1lem  36341  heiborlem3  36345  heiborlem10  36352  heibor  36353  rrndstprj2  36363  cmpidelt  36391  rngoid  36434  fsuppind  40823  limsuc2  41426  cvgdvgrat  42715  cncmpmax  43359  foelrnf  43527  mccllem  43958  mccl  43959  climinf  43967  climsuse  43969  islptre  43980  limcperiod  43989  addlimc  44009  0ellimcdiv  44010  cncficcgt0  44249  dvbdfbdioolem2  44290  ioodvbdlimc1lem2  44293  ioodvbdlimc2lem  44295  dvnprodlem3  44309  stoweidlem7  44368  stoweidlem15  44376  stoweidlem21  44382  stoweidlem31  44392  stoweidlem35  44396  stoweidlem36  44397  stoweidlem50  44411  stoweidlem57  44418  stoweidlem59  44420  wallispilem3  44428  dirkercncflem2  44465  dirkercncflem4  44467  fourierdlem32  44500  fourierdlem33  44501  fourierdlem39  44507  fourierdlem62  44529  fourierdlem71  44538  fourierdlem89  44556  fourierdlem91  44558  fourierdlem93  44560  fourierdlem101  44568  fourierdlem103  44570  fourierdlem104  44571  etransclem24  44619  etransclem32  44627  smflimlem6  45137  smfpimcc  45169  smfsuplem2  45173  isomushgr  46138