Theorem rspccva 3576

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 3573	. 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  4406  n0snor2el  4784  seex  5578  preddowncl  6280  frpoins3g  6294  foelrn  7041  foelrnf  7042  caofid0l  7646  caofid0r  7647  caofid1  7648  caofid2  7649  onnseq  8267  odi  8497  omsmolem  8575  naddssim  8603  fvixp  8829  unblem1  9181  ordiso2  9407  unwdomg  9476  ac5num  9930  acni2  9940  fodomacn  9950  iundom2g  10434  fpwwe2lem3  10527  eltsk2g  10645  tskpwss  10646  tskpw  10647  tsken  10648  prlem934  10927  dedekindle  11280  ltord1  11646  leord1  11647  eqord1  11648  ltord2  11649  leord2  11650  eqord2  11651  supmul1  12094  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  18541  grpinvalem  18547  grpinvex  18822  issubg2  19020  issubg4  19024  nmzbi  19043  gagrpid  19173  cntzi  19208  psgnunilem2  19374  sylow1lem3  19479  pgpfi  19484  slwispgp  19490  sylow2alem1  19496  dprdfcl  19894  ablfac2  19970  abveq0  20703  issrngd  20740  phllmhm  21539  ipcl  21540  ipeq0  21545  isphld  21561  ocvi  21576  pf1ind  22240  cayhamlem3  22772  elcls3  22968  neindisj2  23008  perfi  23040  cnima  23150  1stcfb  23330  1stcelcls  23346  llyi  23359  nllyi  23360  locfinnei  23408  1stckgenlem  23438  ptbasin  23462  txcls  23489  ptcnp  23507  ufli  23799  tgpt0  24004  tsmsxplem2  24039  nrmmetd  24460  tngngp  24540  tngngp3  24542  reperflem  24705  lebnumlem3  24860  htpyi  24871  htpycc  24877  phtpyi  24881  cfili  25166  cmetcvg  25183  caubl  25206  caublcls  25207  bcthlem2  25223  bcthlem3  25224  bcthlem4  25225  ovolicc2lem1  25416  ovolicc2lem5  25420  ovolicc2  25421  voliunlem3  25451  volsuplem  25454  uniioombllem2  25482  mbfima  25529  ismbfd  25538  ismbf3d  25553  mbfmullem  25624  itg2monolem1  25649  itg2i1fseqle  25653  itg2i1fseq  25654  itg2i1fseq2  25655  itg2addlem  25657  bddmulibl  25738  bddiblnc  25741  c1liplem1  25899  dvfsumle  25924  dvfsumleOLD  25925  dvfsumabs  25927  dvfsumrlimf  25929  dvfsumlem1  25930  dvfsumlem2  25931  dvfsumlem2OLD  25932  dvfsumlem3  25933  dvfsumlem4  25934  dvfsumrlimge0  25935  dvfsum2  25939  ftc1lem6  25946  ulmcau  26302  ulmdvlem1  26307  ulmdvlem3  26309  mtestbdd  26312  itgulm  26315  radcnvlem1  26320  abelthlem5  26343  abelthlem7  26346  areambl  26866  2lgslem1a  27300  dchrisumlem2  27399  dchrvmasumiflem1  27410  pntpbnd1  27495  ostthlem1  27536  madebday  27814  addscom  27878  precsexlem9  28122  peano5n0s  28217  zs12bday  28361  tglowdim1i  28446  brbtwn2  28850  ax5seglem1  28873  ax5seglem2  28874  ax5seglem9  28882  axcontlem4  28912  axcontlem12  28920  fusgreghash2wsp  30282  grpoidinvlem3  30450  grpoidinv  30452  grpoidinv2  30459  vcidOLD  30508  minvecolem5  30825  hcaucvg  31130  hlimconvi  31135  lnopeq0i  31951  cnlnadjlem5  32015  csmdsymi  32278  difelsiga  34100  eulerpartlemb  34336  ballotlemfc0  34461  ballotlemfcc  34462  ptpconn  35206  cvmsdisj  35243  cvmshmeo  35244  snmlflim  35305  elmrsubrn  35493  mvtinf  35528  sinccvg  35646  fnemeet1  36340  fnemeet2  36341  fnejoin1  36342  fnejoin2  36343  bj-seex  36896  poimirlem27  37627  poimirlem32  37632  mblfinlem1  37637  ovoliunnfl  37642  ex-ovoliunnfl  37643  voliunnfl  37644  volsupnfl  37645  mbfresfi  37646  itg2gt0cn  37655  ftc1cnnc  37672  ftc1anc  37681  upixp  37709  filbcmb  37720  sdclem1  37723  seqpo  37727  incsequz2  37729  mettrifi  37737  caushft  37741  sstotbnd2  37754  heibor1lem  37789  heiborlem3  37793  heiborlem10  37800  heibor  37801  rrndstprj2  37811  cmpidelt  37839  rngoid  37882  fsuppind  42563  limsuc2  43014  cvgdvgrat  44286  cncmpmax  45010  mccllem  45578  mccl  45579  climinf  45587  climsuse  45589  islptre  45600  limcperiod  45609  addlimc  45629  0ellimcdiv  45630  cncficcgt0  45869  dvbdfbdioolem2  45910  ioodvbdlimc1lem2  45913  ioodvbdlimc2lem  45915  dvnprodlem3  45929  stoweidlem7  45988  stoweidlem15  45996  stoweidlem21  46002  stoweidlem31  46012  stoweidlem35  46016  stoweidlem36  46017  stoweidlem50  46031  stoweidlem57  46038  stoweidlem59  46040  wallispilem3  46048  dirkercncflem2  46085  dirkercncflem4  46087  fourierdlem32  46120  fourierdlem33  46121  fourierdlem39  46127  fourierdlem62  46149  fourierdlem71  46158  fourierdlem89  46176  fourierdlem91  46178  fourierdlem93  46180  fourierdlem101  46188  fourierdlem103  46190  fourierdlem104  46191  etransclem24  46239  etransclem32  46247  smflimlem6  46757  smfpimcc  46789  smfsuplem2  46793  gricushgr  47901