Theorem rspccva 3571

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048

This theorem is referenced by:  disjne  4402  n0snor2el  4782  seex  5573  preddowncl  6279  frpoins3g  6293  foelrn  7040  foelrnf  7041  caofid0l  7643  caofid0r  7644  caofid1  7645  caofid2  7646  onnseq  8264  odi  8494  omsmolem  8572  naddssim  8600  fvixp  8826  unblem1  9176  ordiso2  9401  unwdomg  9470  ac5num  9927  acni2  9937  fodomacn  9947  iundom2g  10431  fpwwe2lem3  10524  eltsk2g  10642  tskpwss  10643  tskpw  10644  tsken  10645  prlem934  10924  dedekindle  11277  ltord1  11643  leord1  11644  eqord1  11645  ltord2  11646  leord2  11647  eqord2  11648  supmul1  12091  seqcaopr2  13945  bccl  14229  hashbc  14360  limsupbnd2  15390  2clim  15479  climsup  15577  caurcvg2  15585  caucvgb  15587  isummulc2  15669  telfsumo2  15710  fsumparts  15713  incexclem  15743  isumshft  15746  climcndslem1  15756  climcndslem2  15757  supcvg  15763  geomulcvg  15783  mertenslem2  15792  mertens  15793  bpolycl  15959  bpolydif  15962  rpnnen2lem10  16132  dvdsprime  16598  fuciso  17885  lubub  18417  lubl  18418  mgmlrid  18575  grpinvalem  18581  grpinvex  18856  issubg2  19054  issubg4  19058  nmzbi  19076  gagrpid  19206  cntzi  19241  psgnunilem2  19407  sylow1lem3  19512  pgpfi  19517  slwispgp  19523  sylow2alem1  19529  dprdfcl  19927  ablfac2  20003  abveq0  20733  issrngd  20770  phllmhm  21569  ipcl  21570  ipeq0  21575  isphld  21591  ocvi  21606  pf1ind  22270  cayhamlem3  22802  elcls3  22998  neindisj2  23038  perfi  23070  cnima  23180  1stcfb  23360  1stcelcls  23376  llyi  23389  nllyi  23390  locfinnei  23438  1stckgenlem  23468  ptbasin  23492  txcls  23519  ptcnp  23537  ufli  23829  tgpt0  24034  tsmsxplem2  24069  nrmmetd  24489  tngngp  24569  tngngp3  24571  reperflem  24734  lebnumlem3  24889  htpyi  24900  htpycc  24906  phtpyi  24910  cfili  25195  cmetcvg  25212  caubl  25235  caublcls  25236  bcthlem2  25252  bcthlem3  25253  bcthlem4  25254  ovolicc2lem1  25445  ovolicc2lem5  25449  ovolicc2  25450  voliunlem3  25480  volsuplem  25483  uniioombllem2  25511  mbfima  25558  ismbfd  25567  ismbf3d  25582  mbfmullem  25653  itg2monolem1  25678  itg2i1fseqle  25682  itg2i1fseq  25683  itg2i1fseq2  25684  itg2addlem  25686  bddmulibl  25767  bddiblnc  25770  c1liplem1  25928  dvfsumle  25953  dvfsumleOLD  25954  dvfsumabs  25956  dvfsumrlimf  25958  dvfsumlem1  25959  dvfsumlem2  25960  dvfsumlem2OLD  25961  dvfsumlem3  25962  dvfsumlem4  25963  dvfsumrlimge0  25964  dvfsum2  25968  ftc1lem6  25975  ulmcau  26331  ulmdvlem1  26336  ulmdvlem3  26338  mtestbdd  26341  itgulm  26344  radcnvlem1  26349  abelthlem5  26372  abelthlem7  26375  areambl  26895  2lgslem1a  27329  dchrisumlem2  27428  dchrvmasumiflem1  27439  pntpbnd1  27524  ostthlem1  27565  madebday  27845  addscom  27909  precsexlem9  28153  peano5n0s  28248  zs12bday  28394  tglowdim1i  28479  brbtwn2  28883  ax5seglem1  28906  ax5seglem2  28907  ax5seglem9  28915  axcontlem4  28945  axcontlem12  28953  fusgreghash2wsp  30318  grpoidinvlem3  30486  grpoidinv  30488  grpoidinv2  30495  vcidOLD  30544  minvecolem5  30861  hcaucvg  31166  hlimconvi  31171  lnopeq0i  31987  cnlnadjlem5  32051  csmdsymi  32314  difelsiga  34146  eulerpartlemb  34381  ballotlemfc0  34506  ballotlemfcc  34507  ptpconn  35277  cvmsdisj  35314  cvmshmeo  35315  snmlflim  35376  elmrsubrn  35564  mvtinf  35599  sinccvg  35717  fnemeet1  36410  fnemeet2  36411  fnejoin1  36412  fnejoin2  36413  bj-seex  36966  poimirlem27  37697  poimirlem32  37702  mblfinlem1  37707  ovoliunnfl  37712  ex-ovoliunnfl  37713  voliunnfl  37714  volsupnfl  37715  mbfresfi  37716  itg2gt0cn  37725  ftc1cnnc  37742  ftc1anc  37751  upixp  37779  filbcmb  37790  sdclem1  37793  seqpo  37797  incsequz2  37799  mettrifi  37807  caushft  37811  sstotbnd2  37824  heibor1lem  37859  heiborlem3  37863  heiborlem10  37870  heibor  37871  rrndstprj2  37881  cmpidelt  37909  rngoid  37952  fsuppind  42693  limsuc2  43144  cvgdvgrat  44416  cncmpmax  45139  mccllem  45707  mccl  45708  climinf  45716  climsuse  45718  islptre  45729  limcperiod  45738  addlimc  45756  0ellimcdiv  45757  cncficcgt0  45996  dvbdfbdioolem2  46037  ioodvbdlimc1lem2  46040  ioodvbdlimc2lem  46042  dvnprodlem3  46056  stoweidlem7  46115  stoweidlem15  46123  stoweidlem21  46129  stoweidlem31  46139  stoweidlem35  46143  stoweidlem36  46144  stoweidlem50  46158  stoweidlem57  46165  stoweidlem59  46167  wallispilem3  46175  dirkercncflem2  46212  dirkercncflem4  46214  fourierdlem32  46247  fourierdlem33  46248  fourierdlem39  46254  fourierdlem62  46276  fourierdlem71  46285  fourierdlem89  46303  fourierdlem91  46305  fourierdlem93  46307  fourierdlem101  46315  fourierdlem103  46317  fourierdlem104  46318  etransclem24  46366  etransclem32  46374  smflimlem6  46884  smfpimcc  46916  smfsuplem2  46920  gricushgr  48027