Theorem rspcdva 3577

Description: Restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 21-Jun-2020.)

Hypotheses

Ref	Expression
rspcdva.1	⊢ (𝑥 = 𝐶 → (𝜓 ↔ 𝜒))
rspcdva.2	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
rspcdva.3	⊢ (𝜑 → 𝐶 ∈ 𝐴)

Assertion

Ref	Expression
rspcdva	⊢ (𝜑 → 𝜒)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝜒,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem rspcdva

Step	Hyp	Ref	Expression
1		rspcdva.3	. 2 ⊢ (𝜑 → 𝐶 ∈ 𝐴)
2		rspcdva.2	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
3		rspcdva.1	. . 3 ⊢ (𝑥 = 𝐶 → (𝜓 ↔ 𝜒))
4	3	rspcv 3572	. 2 ⊢ (𝐶 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝜓 → 𝜒))
5	1, 2, 4	sylc 66	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077

This theorem is used by:  nvocnv  7290  knatar  7368  caofref  7725  caofinvl  7726  tfisi  7871  fnwe2lem3  8150  frxp2  8164  frxp3  8171  suppssov1  8218  suppssov2  8219  fpr3g  8307  fprresex  8332  tfrlem1  8387  tfrlem5  8391  coflton  8684  cofon1  8685  cofon2  8686  marypha1lem  9429  marypha1  9430  ordtypelem6  9521  ordtypelem7  9522  wemaplem2  9545  oemapvali  9689  cantnflem1c  9692  ttrcltr  9721  ttrclss  9725  dmttrcl  9726  rnttrcl  9727  ttrclselem2  9731  scottelrankd  9952  infxpenlem  10096  acni  10128  dfac9  10219  dfac12lem2  10227  sornom  10359  fin1ai  10375  fin2i  10377  fin23lem11  10399  isfin2-2  10401  fin23lem17  10420  fin23lem39  10432  fin1a2lem13  10494  hsmexlem4  10511  ttukeylem5  10595  ttukeylem6  10596  canth4  10736  pwfseqlem5  10752  winalim2  10785  wununi  10795  wunpw  10796  dedekind  11477  zsupss  13068  uzwo3  13074  seqcl2  14167  seqcl  14169  seqf  14170  seqfveq2  14171  seqfveq  14173  seqshft2  14175  monoord  14179  monoord2  14180  sermono  14181  seqsplit  14182  seqcaopr3  14184  seqid  14194  seqid2  14195  seqhomo  14196  seqz  14197  discr1  14387  discr  14388  hashbclem  14601  wrdind  14876  limsupgre  15654  climi  15683  rlimi  15686  rlimclim1  15718  rlimclim  15719  climrlim2  15720  rlimcn1  15761  climcn1  15765  isercoll2  15842  caucvgrlem  15846  caucvgb  15853  iseraltlem2  15856  iseraltlem3  15857  fsumm1  15923  fsum1p  15925  fsumcom2  15946  fsumge1  15970  telfsumo  15975  telfsumo2  15976  fsumparts  15979  o1fsum  15986  isum1p  16016  isumnn0nn  16017  isumrpcl  16018  climcndslem1  16024  climcndslem2  16025  climcnds  16026  cvgrat  16058  mertenslem1  16059  mertens  16061  fprodm1  16140  fprod1p  16141  fprodcom2  16157  prmind2  16866  pcmpt2  17077  prmpwdvds  17088  prmreclem4  17103  prmreclem5  17104  vdwlem1  17165  vdwlem2  17166  vdwlem9  17173  vdwlem10  17174  rami  17199  ramcl  17213  prmodvdslcmf  17231  prmgaplcmlem1  17235  cshwsidrepsw  17277  prdsbasprj  17649  isacs2  17833  acsfiel  17834  catidex  17854  iscatd2  17861  catlid  17863  catrid  17864  subcidcl  18025  funcid  18051  yonedalem4c  18457  yonffthlem  18462  isdrs2  18486  luble  18537  glble  18550  joinle  18564  meetle  18578  poslubmo  18589  posglbmo  18590  acsdrsel  18723  isacs4lem  18724  isacs5lem  18725  acsdrscl  18726  acsficl  18727  chnltm1  18789  chnub  18802  lidrideqd  18856  grpinvalem  18860  grpinva  18861  mndind  19030  grpidd2  19194  mulgsubcl  19304  issubg4  19362  ghmf1  19466  fislw  19845  efgsdmi  19952  efgsrel  19954  gexexlem  20072  gsumzaddlem  20141  gsummhm2  20159  dprdcntz  20230  dprddisj  20231  dprdss  20251  dprd2dlem2  20262  dprd2da  20264  dpjrid  20284  ablfac1eu  20295  pgpfac1lem1  20296  pgpfaclem2  20304  lringuplu  20802  issrngd  21118  islbs2  21438  lbsextlem4  21445  prmidl  21627  prmirredlem  21784  psgndiflemB  21912  frlmphl  22093  mplsubglem  22312  mpllsslem  22313  subrgasclcl  22382  mplind  22385  evlslem1  22397  ply1scleq  22629  mdetralt  22929  mdetunilem1  22933  lmcvg  23586  iscncl  23593  lmff  23625  cnrmi  23684  cmpcov  23713  fiuncmp  23728  hauscmplem  23730  1stcfb  23769  1stcelcls  23786  restnlly  23807  islly2  23809  lly1stc  23821  kgeni  23862  ptpjpre1  23896  ptbasfi  23906  ptpjopn  23937  dfac14  23943  txtube  23965  cnmpt11  23988  cnmpt21  23996  cnmptkp  24005  cnmptk1p  24010  qtopomap  24043  qtopcmap  24044  flimcf  24307  fclscf  24350  flfcntr  24368  ptcmplem3  24379  tgpt0  24444  tsmsi  24459  tsmsxplem2  24479  tsmsxp  24480  isucn2  24603  ucnima  24605  ucncn  24609  cfiluweak  24619  cuspcvg  24625  imasdsf1olem  24698  lpbl  24828  comet  24838  cfilucfil  24884  cnheiborlem  25281  cnheibor  25282  bndth  25285  nmoleub2lem2  25443  nmoleub3  25446  ipcau2  25561  tcphcphlem1  25562  tcphcphlem2  25563  lmmcvg  25588  cmetcaulem  25615  iscmet3lem1  25618  iscmet3lem2  25619  pjthlem1  25764  pjthlem2  25765  ivthlem1  25778  ivthlem2  25779  ivthlem3  25780  ivth2  25782  ivthle  25783  ivthle2  25784  ivthicc  25785  ovoliunlem1  25829  ovolshftlem1  25836  ovolscalem1  25840  ovolicc2lem3  25846  ovolicc2lem4  25847  ovolicc2  25849  volsup  25883  dyadmbl  25927  vitalilem2  25936  vitalilem3  25937  mbfdm  25953  ismbf3d  25981  cncombf  25985  itg2seq  26069  itg2monolem2  26078  itg2monolem3  26079  itg2mono  26080  iblitg  26095  itgconst  26145  itgfsum  26153  limcvallem  26197  cnlimci  26215  cnmptlimc  26216  dvferm1lem  26310  dvferm1  26311  dvferm2lem  26312  dvferm2  26313  dvlipcn  26320  dvle  26333  lhop1lem  26339  dvfsumge  26348  dvfsumlem2  26353  dvfsumlem3  26354  ftc1a  26363  ftc1lem4  26365  itgsubstlem  26374  mdeglt  26389  deg1lt  26421  ply1divex  26461  fta1glem2  26493  fta1g  26494  plyco0  26516  plyeq0lem  26535  dgrcolem2  26599  plydivlem4  26623  plydivex  26624  fta1lem  26634  vieta1lem2  26640  vieta1  26641  tayl0  26695  ulmi  26719  ulmdvlem1  26733  ulmdvlem3  26735  ulmdv  26736  mtest  26737  pserulm  26755  efif1olem4  26879  rlimcnp  27299  rlimcnp2  27300  xrlimcnp  27302  scvxcvx  27319  lgamgulmlem5  27366  lgambdd  27370  lgamcvglem  27373  wilthlem2  27402  fsumdvdscom  27518  musumsum  27525  chtub  27545  fsumvma  27546  perfectlem2  27563  dchrelbas3  27571  dchrelbasd  27572  dchrn0  27583  dchrptlem2  27598  lgsval2lem  27640  lgsdirnn0  27677  lgsdinn0  27678  2sqlem10  27761  dchrisumlem1  27822  dchrmusum2  27827  dchrvmasumlem2  27831  dchrvmasumlem3  27832  dchrvmasumiflem1  27834  dchrisum0flblem2  27842  dchrisum0flb  27843  dchrisum0lem1b  27848  dchrisum0lem2  27851  2vmadivsumlem  27873  chpdifbndlem1  27886  selberg3lem1  27890  selberg4lem1  27893  pntrsumbnd2  27900  pntrlog2bndlem2  27911  pntrlog2bndlem3  27912  pntrlog2bndlem5  27914  pntrlog2bndlem6  27916  pntibndlem2  27924  pntibndlem3  27925  pntlemn  27933  pntlemj  27936  pntlemi  27937  pntlemo  27940  pntleme  27941  pntlem3  27942  pntlemp  27943  ostth2lem1  27951  ostthlem1  27960  ostth2lem2  27967  ostth3  27971  nosupprefixmo  28063  noinfprefixmo  28064  noinfbnd1lem1  28086  noinfbnd1lem4  28089  noinfbnd2lem1  28093  noinfbnd2  28094  eqcuts3  28196  cofslts  28310  coinitslts  28311  leadds1  28381  addsass  28397  addbdaylem  28409  negsid  28433  mulscom  28531  addsdilem3  28545  addsdilem4  28546  mulsasslem3  28557  precsexlem8  28606  precsexlem9  28607  precsexlem11  28609  addonbday  28671  n0fincut  28747  onsfi  28748  bdayfinbndlem1  28859  bdayfinbnd  28861  tglowdim1i  28970  tglowdim2ln  29126  wlkonl1iedg  30250  wlkp1lem7  30264  wlkp1lem8  30265  revwlk  30273  crctcshwlkn0lem6  30410  eupth2eucrct  30824  eupth2lem3  30843  ubthlem1  31478  ubthlem2  31479  minvecolem3  31484  occllem  31911  pjhthlem1  31999  eqelbid  33119  fnfvor  33251  ofrco  33252  wrdt2ind  33563  mgccole1  33598  mgcmnt2  33601  dfmgc2  33604  fxpgaeq  33777  fxpsubm  33780  fxpsubg  33781  fxpsubrg  33782  elrgspnlem4  33853  elrgspnsubrunlem2  33856  0nellinds  33973  linds2eq  33983  elrspunidl  34025  mxidlmax  34037  ssmxidl  34046  1arithidomlem1  34114  1arithidom  34116  1arithufdlem3  34125  1arithufdlem4  34126  ply1dg1rt  34159  vietalem  34258  lbsdiflsp0  34305  fedgmullem1  34308  fedgmullem2  34309  extdg1id  34345  fldextrspunlsplem  34352  extdgfialglem2  34372  constrsscn  34419  constrconj  34424  zrhcntr  34658  ofcfeqd2  34780  inelpisys  34834  unelldsys  34838  ldgenpisyslem1  34843  mbfmcnvima  34935  signstfvneq0  35248  fsum2dsub  35283  hgt750lemc  35323  hgt750lemd  35324  hgt749d  35325  hgt750lemf  35329  bnj1379  35507  bnj1450  35727  subfacp1lem5  36036  cvmlift2lem10  36164  nmulprop  37032  nmulcom  37036  nadddilem1  37062  nadddilem3  37064  weiunfrlem  37345  weiunpo  37346  weiunso  37347  weiunfr  37348  weiunse  37349  mh-inf3f1  37422  unblimceq0lem  37465  unblimceq0  37466  unbdqndv2  37470  bj-ismoored  38121  lcmineqlem4  43176  dvle2  43216  aks4d1p9  43232  primrootlekpowne0  43249  aks6d1c1p3  43254  aks6d1c1p4  43255  aks6d1c1p5  43256  aks6d1c1  43260  hashscontpow  43266  aks6d1c2lem3  43270  sticksstones1  43290  aks6d1c6lem1  43314  aks6d1c6lem2  43315  aks6d1c6lem4  43317  aks6d1c7  43328  aks5lem3a  43333  unitscyglem1  43339  unitscyglem2  43340  unitscyglem3  43341  unitscyglem4  43342  exfinfldd  43347  aomclem4  44153  mnuop123d  45340  mnuprdlem1  45350  mnuprdlem2  45351  eliind  46182  rnmptbd2lem  46354  rnmptbdlem  46361  cvgcau  46594  limclner  46755  climisp  46850  climrescn  46852  climxrrelem  46853  climxrre  46854  liminflelimsuplem  46879  cncfshift  46978  cncfperiod  46983  fperdvper  47023  fourierdlem48  47258  salunicl  47420  saldifcl  47423  meadjuni  47561  chnerlem1  47986  lubsscl  50168  glbsscl  50169  ipolub  50196  ipoglb  50199  ssccatid  50280  upciclem1  50376  oppcup3lem  50416  oppcthinendcALT  50670  setcthin  50694  veroquadmodzerod  51153