Theorem rspcdva 3571

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 3566	. 2 ⊢ (𝐶 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝜓 → 𝜒))
5	1, 2, 4	sylc 65	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540   ∈ wcel 2105  ∀wral 3061

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3062

This theorem is referenced by:  nvocnv  7203  knatar  7278  caofref  7616  caofinvl  7617  tfisi  7765  suppssov1  8076  fpr3g  8163  fprresex  8188  wfrlem17OLD  8218  tfrlem1  8269  tfrlem5  8273  marypha1lem  9282  marypha1  9283  ordtypelem6  9372  ordtypelem7  9373  wemaplem2  9396  oemapvali  9533  cantnflem1c  9536  ttrcltr  9565  ttrclss  9569  dmttrcl  9570  rnttrcl  9571  ttrclselem2  9575  infxpenlem  9862  acni  9894  dfac9  9985  dfac12lem2  9993  sornom  10126  fin1ai  10142  fin2i  10144  fin23lem11  10166  isfin2-2  10168  fin23lem17  10187  fin23lem39  10199  fin1a2lem13  10261  hsmexlem4  10278  ttukeylem5  10362  ttukeylem6  10363  canth4  10496  pwfseqlem5  10512  winalim2  10545  wununi  10555  wunpw  10556  dedekind  11231  zsupss  12770  uzwo3  12776  seqcl2  13834  seqcl  13836  seqf  13837  seqfveq2  13838  seqfveq  13840  seqshft2  13842  monoord  13846  monoord2  13847  sermono  13848  seqsplit  13849  seqcaopr3  13851  seqid  13861  seqid2  13862  seqhomo  13863  seqz  13864  discr1  14047  discr  14048  hashbclem  14256  wrdind  14525  limsupgre  15281  climi  15310  rlimi  15313  rlimclim1  15345  rlimclim  15346  climrlim2  15347  rlimcn1  15388  climcn1  15392  isercoll2  15471  caucvgrlem  15475  caucvgb  15482  iseraltlem2  15485  iseraltlem3  15486  fsumm1  15554  fsum1p  15556  fsumcom2  15577  fsumge1  15600  telfsumo  15605  telfsumo2  15606  fsumparts  15609  o1fsum  15616  isum1p  15644  isumnn0nn  15645  isumrpcl  15646  climcndslem1  15652  climcndslem2  15653  climcnds  15654  cvgrat  15686  mertenslem1  15687  mertens  15689  fprodm1  15768  fprod1p  15769  fprodcom2  15785  prmind2  16479  pcmpt2  16683  prmpwdvds  16694  prmreclem4  16709  prmreclem5  16710  vdwlem1  16771  vdwlem2  16772  vdwlem9  16779  vdwlem10  16780  rami  16805  ramcl  16819  prmodvdslcmf  16837  prmgaplcmlem1  16841  cshwsidrepsw  16884  prdsbasprj  17272  isacs2  17451  acsfiel  17452  catidex  17472  iscatd2  17479  catlid  17481  catrid  17482  subcidcl  17648  funcid  17674  yonedalem4c  18084  yonffthlem  18089  isdrs2  18113  luble  18166  glble  18179  joinle  18193  meetle  18207  poslubmo  18218  posglbmo  18219  acsdrsel  18350  isacs4lem  18351  isacs5lem  18352  acsdrscl  18353  acsficl  18354  lidrideqd  18442  grprinvlem  18446  grprinvd  18447  mndind  18555  grpidd2  18705  mulgsubcl  18806  issubg4  18862  ghmf1  18951  fislw  19318  efgsdmi  19425  efgsrel  19427  gexexlem  19540  gsumzaddlem  19609  gsummhm2  19627  dprdcntz  19698  dprddisj  19699  dprdss  19719  dprd2dlem2  19730  dprd2da  19732  dpjrid  19752  ablfac1eu  19763  pgpfac1lem1  19764  pgpfaclem2  19772  issrngd  20219  islbs2  20514  lbsextlem4  20521  prmirredlem  20792  psgndiflemB  20903  frlmphl  21086  mplsubglem  21303  mpllsslem  21304  subrgasclcl  21373  mplind  21376  evlslem1  21390  mdetralt  21855  mdetunilem1  21859  lmcvg  22511  iscncl  22518  lmff  22550  cnrmi  22609  cmpcov  22638  fiuncmp  22653  hauscmplem  22655  1stcfb  22694  1stcelcls  22710  restnlly  22731  islly2  22733  lly1stc  22745  kgeni  22786  ptpjpre1  22820  ptbasfi  22830  ptpjopn  22861  dfac14  22867  txtube  22889  cnmpt11  22912  cnmpt21  22920  cnmptkp  22929  cnmptk1p  22934  qtopomap  22967  qtopcmap  22968  flimcf  23231  fclscf  23274  flfcntr  23292  ptcmplem3  23303  tgpt0  23368  tsmsi  23383  tsmsxplem2  23403  tsmsxp  23404  isucn2  23529  ucnima  23531  ucncn  23535  cfiluweak  23545  cuspcvg  23551  imasdsf1olem  23624  lpbl  23757  comet  23767  cfilucfil  23813  cnheiborlem  24215  cnheibor  24216  bndth  24219  nmoleub2lem2  24377  nmoleub3  24380  ipcau2  24496  tcphcphlem1  24497  tcphcphlem2  24498  lmmcvg  24523  cmetcaulem  24550  iscmet3lem1  24553  iscmet3lem2  24554  pjthlem1  24699  pjthlem2  24700  ivthlem1  24713  ivthlem2  24714  ivthlem3  24715  ivth2  24717  ivthle  24718  ivthle2  24719  ivthicc  24720  ovoliunlem1  24764  ovolshftlem1  24771  ovolscalem1  24775  ovolicc2lem3  24781  ovolicc2lem4  24782  ovolicc2  24784  volsup  24818  dyadmbl  24862  vitalilem2  24871  vitalilem3  24872  mbfdm  24888  ismbf3d  24916  cncombf  24920  itg2seq  25005  itg2monolem2  25014  itg2monolem3  25015  itg2mono  25016  iblitg  25031  itgconst  25081  itgfsum  25089  limcvallem  25133  cnlimci  25151  cnmptlimc  25152  dvferm1lem  25246  dvferm1  25247  dvferm2lem  25248  dvferm2  25249  dvlipcn  25256  dvle  25269  lhop1lem  25275  dvfsumge  25284  dvfsumlem2  25289  dvfsumlem3  25290  ftc1a  25299  ftc1lem4  25301  itgsubstlem  25310  mdeglt  25328  deg1lt  25360  ply1divex  25399  fta1glem2  25429  fta1g  25430  plyco0  25451  plyeq0lem  25469  dgrcolem2  25533  plydivlem4  25554  plydivex  25555  fta1lem  25565  vieta1lem2  25569  vieta1  25570  tayl0  25619  ulmi  25643  ulmdvlem1  25657  ulmdvlem3  25659  ulmdv  25660  mtest  25661  pserulm  25679  efif1olem4  25799  rlimcnp  26213  rlimcnp2  26214  xrlimcnp  26216  scvxcvx  26233  lgamgulmlem5  26280  lgambdd  26284  lgamcvglem  26287  wilthlem2  26316  fsumdvdscom  26432  musumsum  26439  chtub  26458  fsumvma  26459  perfectlem2  26476  dchrelbas3  26484  dchrelbasd  26485  dchrn0  26496  dchrptlem2  26511  lgsval2lem  26553  lgsdirnn0  26590  lgsdinn0  26591  2sqlem10  26674  dchrisumlem1  26735  dchrmusum2  26740  dchrvmasumlem2  26744  dchrvmasumlem3  26745  dchrvmasumiflem1  26747  dchrisum0flblem2  26755  dchrisum0flb  26756  dchrisum0lem1b  26761  dchrisum0lem2  26764  2vmadivsumlem  26786  chpdifbndlem1  26799  selberg3lem1  26803  selberg4lem1  26806  pntrsumbnd2  26813  pntrlog2bndlem2  26824  pntrlog2bndlem3  26825  pntrlog2bndlem5  26827  pntrlog2bndlem6  26829  pntibndlem2  26837  pntibndlem3  26838  pntlemn  26846  pntlemj  26849  pntlemi  26850  pntlemo  26853  pntleme  26854  pntlem3  26855  pntlemp  26856  ostth2lem1  26864  ostthlem1  26873  ostth2lem2  26880  ostth3  26884  nosupprefixmo  26946  noinfprefixmo  26947  noinfbnd1lem1  26969  noinfbnd1lem4  26972  noinfbnd2lem1  26976  noinfbnd2  26977  tglowdim1i  27092  tglowdim2ln  27242  wlkonl1iedg  28262  wlkp1lem7  28276  wlkp1lem8  28277  crctcshwlkn0lem6  28409  eupth2eucrct  28810  eupth2lem3  28829  ubthlem1  29461  ubthlem2  29462  minvecolem3  29467  occllem  29894  pjhthlem1  29982  wrdt2ind  31453  mgccole1  31496  mgcmnt2  31499  dfmgc2  31502  0nellinds  31804  linds2eq  31813  elrspunidl  31844  prmidl  31853  mxidlmax  31875  ssmxidl  31880  ply1scleq  31906  lbsdiflsp0  31946  fedgmullem1  31949  fedgmullem2  31950  extdg1id  31977  ofcfeqd2  32308  inelpisys  32361  unelldsys  32365  ldgenpisyslem1  32370  mbfmcnvima  32463  signstfvneq0  32792  fsum2dsub  32828  hgt750lemc  32868  hgt750lemd  32869  hgt749d  32870  hgt750lemf  32874  bnj1379  33050  bnj1450  33270  revwlk  33326  subfacp1lem5  33386  cvmlift2lem10  33514  frxp2  34017  frxp3  34023  cofsslt  34179  coinitsslt  34180  unblimceq0lem  34777  unblimceq0  34778  unbdqndv2  34782  bj-ismoored  35376  lcmineqlem4  40287  dvle2  40327  aks4d1p9  40343  sticksstones1  40352  fnwe2lem2  41127  aomclem4  41133  scottelrankd  42175  mnuop123d  42190  mnuprdlem1  42200  mnuprdlem2  42201  eliind  42928  rnmptbd2lem  43111  rnmptbdlem  43118  limclner  43517  climisp  43612  climrescn  43614  climxrrelem  43615  climxrre  43616  cncfshift  43740  cncfperiod  43745  fperdvper  43785  salunicl  44182  saldifcl  44185  meadjuni  44321  lubsscl  46594  glbsscl  46595  ipolub  46614  ipoglb  46617  setcthin  46676