Theorem rspcdva 3561

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ∈ wcel 2119  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054

This theorem is referenced by:  nvocnv  7225  knatar  7301  caofref  7651  caofinvl  7652  tfisi  7799  frxp2  8084  frxp3  8091  suppssov1  8137  suppssov2  8138  fpr3g  8225  fprresex  8250  tfrlem1  8305  tfrlem5  8309  coflton  8597  cofon1  8598  cofon2  8599  marypha1lem  9336  marypha1  9337  ordtypelem6  9428  ordtypelem7  9429  wemaplem2  9452  oemapvali  9596  cantnflem1c  9599  ttrcltr  9628  ttrclss  9632  dmttrcl  9633  rnttrcl  9634  ttrclselem2  9638  infxpenlem  9926  acni  9958  dfac9  10050  dfac12lem2  10058  sornom  10190  fin1ai  10206  fin2i  10208  fin23lem11  10230  isfin2-2  10232  fin23lem17  10251  fin23lem39  10263  fin1a2lem13  10325  hsmexlem4  10342  ttukeylem5  10426  ttukeylem6  10427  canth4  10561  pwfseqlem5  10577  winalim2  10610  wununi  10620  wunpw  10621  dedekind  11300  zsupss  12878  uzwo3  12884  seqcl2  13973  seqcl  13975  seqf  13976  seqfveq2  13977  seqfveq  13979  seqshft2  13981  monoord  13985  monoord2  13986  sermono  13987  seqsplit  13988  seqcaopr3  13990  seqid  14000  seqid2  14001  seqhomo  14002  seqz  14003  discr1  14192  discr  14193  hashbclem  14405  wrdind  14675  limsupgre  15434  climi  15463  rlimi  15466  rlimclim1  15498  rlimclim  15499  climrlim2  15500  rlimcn1  15541  climcn1  15545  isercoll2  15622  caucvgrlem  15626  caucvgb  15633  iseraltlem2  15636  iseraltlem3  15637  fsumm1  15704  fsum1p  15706  fsumcom2  15727  fsumge1  15751  telfsumo  15756  telfsumo2  15757  fsumparts  15760  o1fsum  15767  isum1p  15797  isumnn0nn  15798  isumrpcl  15799  climcndslem1  15805  climcndslem2  15806  climcnds  15807  cvgrat  15839  mertenslem1  15840  mertens  15842  fprodm1  15923  fprod1p  15924  fprodcom2  15940  prmind2  16645  pcmpt2  16855  prmpwdvds  16866  prmreclem4  16881  prmreclem5  16882  vdwlem1  16943  vdwlem2  16944  vdwlem9  16951  vdwlem10  16952  rami  16977  ramcl  16991  prmodvdslcmf  17009  prmgaplcmlem1  17013  cshwsidrepsw  17055  prdsbasprj  17426  isacs2  17610  acsfiel  17611  catidex  17631  iscatd2  17638  catlid  17640  catrid  17641  subcidcl  17802  funcid  17828  yonedalem4c  18234  yonffthlem  18239  isdrs2  18263  luble  18314  glble  18327  joinle  18341  meetle  18355  poslubmo  18366  posglbmo  18367  acsdrsel  18500  isacs4lem  18501  isacs5lem  18502  acsdrscl  18503  acsficl  18504  chnltm1  18566  chnub  18579  lidrideqd  18628  grpinvalem  18632  grpinva  18633  mndind  18787  grpidd2  18944  mulgsubcl  19055  issubg4  19112  ghmf1  19212  fislw  19591  efgsdmi  19698  efgsrel  19700  gexexlem  19818  gsumzaddlem  19887  gsummhm2  19905  dprdcntz  19976  dprddisj  19977  dprdss  19997  dprd2dlem2  20008  dprd2da  20010  dpjrid  20030  ablfac1eu  20041  pgpfac1lem1  20042  pgpfaclem2  20050  lringuplu  20516  issrngd  20827  islbs2  21147  lbsextlem4  21154  prmirredlem  21447  psgndiflemB  21575  frlmphl  21756  mplsubglem  21973  mpllsslem  21974  subrgasclcl  22043  mplind  22046  evlslem1  22058  ply1scleq  22291  mdetralt  22591  mdetunilem1  22595  lmcvg  23245  iscncl  23252  lmff  23284  cnrmi  23343  cmpcov  23372  fiuncmp  23387  hauscmplem  23389  1stcfb  23428  1stcelcls  23444  restnlly  23465  islly2  23467  lly1stc  23479  kgeni  23520  ptpjpre1  23554  ptbasfi  23564  ptpjopn  23595  dfac14  23601  txtube  23623  cnmpt11  23646  cnmpt21  23654  cnmptkp  23663  cnmptk1p  23668  qtopomap  23701  qtopcmap  23702  flimcf  23965  fclscf  24008  flfcntr  24026  ptcmplem3  24037  tgpt0  24102  tsmsi  24117  tsmsxplem2  24137  tsmsxp  24138  isucn2  24261  ucnima  24263  ucncn  24267  cfiluweak  24277  cuspcvg  24283  imasdsf1olem  24356  lpbl  24486  comet  24496  cfilucfil  24542  cnheiborlem  24939  cnheibor  24940  bndth  24943  nmoleub2lem2  25101  nmoleub3  25104  ipcau2  25219  tcphcphlem1  25220  tcphcphlem2  25221  lmmcvg  25246  cmetcaulem  25273  iscmet3lem1  25276  iscmet3lem2  25277  pjthlem1  25422  pjthlem2  25423  ivthlem1  25436  ivthlem2  25437  ivthlem3  25438  ivth2  25440  ivthle  25441  ivthle2  25442  ivthicc  25443  ovoliunlem1  25487  ovolshftlem1  25494  ovolscalem1  25498  ovolicc2lem3  25504  ovolicc2lem4  25505  ovolicc2  25507  volsup  25541  dyadmbl  25585  vitalilem2  25594  vitalilem3  25595  mbfdm  25611  ismbf3d  25639  cncombf  25643  itg2seq  25727  itg2monolem2  25736  itg2monolem3  25737  itg2mono  25738  iblitg  25753  itgconst  25804  itgfsum  25812  limcvallem  25856  cnlimci  25874  cnmptlimc  25875  dvferm1lem  25969  dvferm1  25970  dvferm2lem  25971  dvferm2  25972  dvlipcn  25979  dvle  25992  lhop1lem  25998  dvfsumge  26007  dvfsumlem2  26012  dvfsumlem3  26013  ftc1a  26022  ftc1lem4  26024  itgsubstlem  26033  mdeglt  26048  deg1lt  26080  ply1divex  26120  fta1glem2  26152  fta1g  26153  plyco0  26175  plyeq0lem  26193  dgrcolem2  26257  plydivlem4  26280  plydivex  26281  fta1lem  26291  vieta1lem2  26295  vieta1  26296  tayl0  26345  ulmi  26369  ulmdvlem1  26383  ulmdvlem3  26385  ulmdv  26386  mtest  26387  pserulm  26405  efif1olem4  26527  rlimcnp  26947  rlimcnp2  26948  xrlimcnp  26950  scvxcvx  26967  lgamgulmlem5  27014  lgambdd  27018  lgamcvglem  27021  wilthlem2  27050  fsumdvdscom  27166  musumsum  27173  chtub  27193  fsumvma  27194  perfectlem2  27211  dchrelbas3  27219  dchrelbasd  27220  dchrn0  27231  dchrptlem2  27246  lgsval2lem  27288  lgsdirnn0  27325  lgsdinn0  27326  2sqlem10  27409  dchrisumlem1  27470  dchrmusum2  27475  dchrvmasumlem2  27479  dchrvmasumlem3  27480  dchrvmasumiflem1  27482  dchrisum0flblem2  27490  dchrisum0flb  27491  dchrisum0lem1b  27496  dchrisum0lem2  27499  2vmadivsumlem  27521  chpdifbndlem1  27534  selberg3lem1  27538  selberg4lem1  27541  pntrsumbnd2  27548  pntrlog2bndlem2  27559  pntrlog2bndlem3  27560  pntrlog2bndlem5  27562  pntrlog2bndlem6  27564  pntibndlem2  27572  pntibndlem3  27573  pntlemn  27581  pntlemj  27584  pntlemi  27585  pntlemo  27588  pntleme  27589  pntlem3  27590  pntlemp  27591  ostth2lem1  27599  ostthlem1  27608  ostth2lem2  27615  ostth3  27619  nosupprefixmo  27682  noinfprefixmo  27683  noinfbnd1lem1  27705  noinfbnd1lem4  27708  noinfbnd2lem1  27712  noinfbnd2  27713  eqcuts3  27814  cofslts  27928  coinitslts  27929  leadds1  27999  addsass  28015  addbdaylem  28027  negsid  28051  mulscom  28149  addsdilem3  28163  addsdilem4  28164  mulsasslem3  28175  precsexlem8  28224  precsexlem9  28225  precsexlem11  28227  addonbday  28289  n0fincut  28365  onsfi  28366  bdayfinbndlem1  28477  bdayfinbnd  28479  tglowdim1i  28587  tglowdim2ln  28737  wlkonl1iedg  29750  wlkp1lem7  29764  wlkp1lem8  29765  crctcshwlkn0lem6  29901  eupth2eucrct  30305  eupth2lem3  30324  ubthlem1  30959  ubthlem2  30960  minvecolem3  30965  occllem  31392  pjhthlem1  31480  eqelbid  32562  fnfvor  32701  ofrco  32702  wrdt2ind  33032  mgccole1  33069  mgcmnt2  33072  dfmgc2  33075  fxpgaeq  33250  fxpsubm  33253  fxpsubg  33254  fxpsubrg  33255  elrgspnlem4  33326  elrgspnsubrunlem2  33329  0nellinds  33453  linds2eq  33464  elrspunidl  33511  prmidl  33523  mxidlmax  33548  ssmxidl  33557  1arithidomlem1  33618  1arithidom  33620  1arithufdlem3  33629  1arithufdlem4  33630  ply1dg1rt  33663  vietalem  33763  lbsdiflsp0  33810  fedgmullem1  33813  fedgmullem2  33814  extdg1id  33850  fldextrspunlsplem  33857  extdgfialglem2  33877  constrsscn  33924  constrconj  33929  zrhcntr  34163  ofcfeqd2  34285  inelpisys  34338  unelldsys  34342  ldgenpisyslem1  34347  mbfmcnvima  34439  signstfvneq0  34756  fsum2dsub  34791  hgt750lemc  34831  hgt750lemd  34832  hgt749d  34833  hgt750lemf  34837  bnj1379  35012  bnj1450  35232  revwlk  35353  subfacp1lem5  35412  cvmlift2lem10  35540  weiunfrlem  36692  weiunpo  36693  weiunso  36694  weiunfr  36695  weiunse  36696  unblimceq0lem  36812  unblimceq0  36813  unbdqndv2  36817  bj-ismoored  37465  lcmineqlem4  42517  dvle2  42557  aks4d1p9  42573  primrootlekpowne0  42590  aks6d1c1p3  42595  aks6d1c1p4  42596  aks6d1c1p5  42597  aks6d1c1  42601  hashscontpow  42607  aks6d1c2lem3  42611  sticksstones1  42631  aks6d1c6lem1  42655  aks6d1c6lem2  42656  aks6d1c6lem4  42658  aks6d1c7  42669  aks5lem3a  42674  unitscyglem1  42680  unitscyglem2  42681  unitscyglem3  42682  unitscyglem4  42683  exfinfldd  42688  fnwe2lem2  43496  aomclem4  43502  scottelrankd  44691  mnuop123d  44706  mnuprdlem1  44716  mnuprdlem2  44717  eliind  45519  rnmptbd2lem  45692  rnmptbdlem  45699  cvgcau  45933  limclner  46094  climisp  46189  climrescn  46191  climxrrelem  46192  climxrre  46193  liminflelimsuplem  46218  cncfshift  46317  cncfperiod  46322  fperdvper  46362  salunicl  46759  saldifcl  46762  meadjuni  46900  chnerlem1  47327  lubsscl  49450  glbsscl  49451  ipolub  49478  ipoglb  49481  ssccatid  49562  upciclem1  49656  oppcup3lem  49696  oppcthinendcALT  49931  setcthin  49955