Theorem rspcdva 3562

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1548   ∈ wcel 2121  ∀wral 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ral 3056

This theorem is referenced by:  nvocnv  7228  knatar  7304  caofref  7654  caofinvl  7655  tfisi  7802  frxp2  8086  frxp3  8093  suppssov1  8139  suppssov2  8140  fpr3g  8228  fprresex  8253  tfrlem1  8308  tfrlem5  8312  coflton  8601  cofon1  8602  cofon2  8603  marypha1lem  9340  marypha1  9341  ordtypelem6  9432  ordtypelem7  9433  wemaplem2  9456  oemapvali  9600  cantnflem1c  9603  ttrcltr  9632  ttrclss  9636  dmttrcl  9637  rnttrcl  9638  ttrclselem2  9642  infxpenlem  9930  acni  9962  dfac9  10054  dfac12lem2  10062  sornom  10195  fin1ai  10211  fin2i  10213  fin23lem11  10235  isfin2-2  10237  fin23lem17  10256  fin23lem39  10268  fin1a2lem13  10330  hsmexlem4  10347  ttukeylem5  10431  ttukeylem6  10432  canth4  10566  pwfseqlem5  10582  winalim2  10615  wununi  10625  wunpw  10626  dedekind  11305  zsupss  12882  uzwo3  12888  seqcl2  13977  seqcl  13979  seqf  13980  seqfveq2  13981  seqfveq  13983  seqshft2  13985  monoord  13989  monoord2  13990  sermono  13991  seqsplit  13992  seqcaopr3  13994  seqid  14004  seqid2  14005  seqhomo  14006  seqz  14007  discr1  14196  discr  14197  hashbclem  14409  wrdind  14679  limsupgre  15438  climi  15467  rlimi  15470  rlimclim1  15502  rlimclim  15503  climrlim2  15504  rlimcn1  15545  climcn1  15549  isercoll2  15626  caucvgrlem  15630  caucvgb  15637  iseraltlem2  15640  iseraltlem3  15641  fsumm1  15708  fsum1p  15710  fsumcom2  15731  fsumge1  15755  telfsumo  15760  telfsumo2  15761  fsumparts  15764  o1fsum  15771  isum1p  15801  isumnn0nn  15802  isumrpcl  15803  climcndslem1  15809  climcndslem2  15810  climcnds  15811  cvgrat  15843  mertenslem1  15844  mertens  15846  fprodm1  15927  fprod1p  15928  fprodcom2  15944  prmind2  16649  pcmpt2  16859  prmpwdvds  16870  prmreclem4  16885  prmreclem5  16886  vdwlem1  16947  vdwlem2  16948  vdwlem9  16955  vdwlem10  16956  rami  16981  ramcl  16995  prmodvdslcmf  17013  prmgaplcmlem1  17017  cshwsidrepsw  17059  prdsbasprj  17430  isacs2  17614  acsfiel  17615  catidex  17635  iscatd2  17642  catlid  17644  catrid  17645  subcidcl  17806  funcid  17832  yonedalem4c  18238  yonffthlem  18243  isdrs2  18267  luble  18318  glble  18331  joinle  18345  meetle  18359  poslubmo  18370  posglbmo  18371  acsdrsel  18504  isacs4lem  18505  isacs5lem  18506  acsdrscl  18507  acsficl  18508  chnltm1  18570  chnub  18583  lidrideqd  18632  grpinvalem  18636  grpinva  18637  mndind  18791  grpidd2  18948  mulgsubcl  19059  issubg4  19116  ghmf1  19215  fislw  19594  efgsdmi  19701  efgsrel  19703  gexexlem  19821  gsumzaddlem  19890  gsummhm2  19908  dprdcntz  19979  dprddisj  19980  dprdss  20000  dprd2dlem2  20011  dprd2da  20013  dpjrid  20033  ablfac1eu  20044  pgpfac1lem1  20045  pgpfaclem2  20053  lringuplu  20519  issrngd  20830  islbs2  21150  lbsextlem4  21157  prmirredlem  21450  psgndiflemB  21578  frlmphl  21759  mplsubglem  21976  mpllsslem  21977  subrgasclcl  22046  mplind  22049  evlslem1  22061  ply1scleq  22294  mdetralt  22594  mdetunilem1  22598  lmcvg  23248  iscncl  23255  lmff  23287  cnrmi  23346  cmpcov  23375  fiuncmp  23390  hauscmplem  23392  1stcfb  23431  1stcelcls  23447  restnlly  23468  islly2  23470  lly1stc  23482  kgeni  23523  ptpjpre1  23557  ptbasfi  23567  ptpjopn  23598  dfac14  23604  txtube  23626  cnmpt11  23649  cnmpt21  23657  cnmptkp  23666  cnmptk1p  23671  qtopomap  23704  qtopcmap  23705  flimcf  23968  fclscf  24011  flfcntr  24029  ptcmplem3  24040  tgpt0  24105  tsmsi  24120  tsmsxplem2  24140  tsmsxp  24141  isucn2  24264  ucnima  24266  ucncn  24270  cfiluweak  24280  cuspcvg  24286  imasdsf1olem  24359  lpbl  24489  comet  24499  cfilucfil  24545  cnheiborlem  24942  cnheibor  24943  bndth  24946  nmoleub2lem2  25104  nmoleub3  25107  ipcau2  25222  tcphcphlem1  25223  tcphcphlem2  25224  lmmcvg  25249  cmetcaulem  25276  iscmet3lem1  25279  iscmet3lem2  25280  pjthlem1  25425  pjthlem2  25426  ivthlem1  25439  ivthlem2  25440  ivthlem3  25441  ivth2  25443  ivthle  25444  ivthle2  25445  ivthicc  25446  ovoliunlem1  25490  ovolshftlem1  25497  ovolscalem1  25501  ovolicc2lem3  25507  ovolicc2lem4  25508  ovolicc2  25510  volsup  25544  dyadmbl  25588  vitalilem2  25597  vitalilem3  25598  mbfdm  25614  ismbf3d  25642  cncombf  25646  itg2seq  25730  itg2monolem2  25739  itg2monolem3  25740  itg2mono  25741  iblitg  25756  itgconst  25807  itgfsum  25815  limcvallem  25859  cnlimci  25877  cnmptlimc  25878  dvferm1lem  25972  dvferm1  25973  dvferm2lem  25974  dvferm2  25975  dvlipcn  25982  dvle  25995  lhop1lem  26001  dvfsumge  26010  dvfsumlem2  26015  dvfsumlem3  26016  ftc1a  26025  ftc1lem4  26027  itgsubstlem  26036  mdeglt  26051  deg1lt  26083  ply1divex  26123  fta1glem2  26155  fta1g  26156  plyco0  26178  plyeq0lem  26196  dgrcolem2  26260  plydivlem4  26283  plydivex  26284  fta1lem  26294  vieta1lem2  26298  vieta1  26299  tayl0  26348  ulmi  26372  ulmdvlem1  26386  ulmdvlem3  26388  ulmdv  26389  mtest  26390  pserulm  26408  efif1olem4  26530  rlimcnp  26950  rlimcnp2  26951  xrlimcnp  26953  scvxcvx  26970  lgamgulmlem5  27017  lgambdd  27021  lgamcvglem  27024  wilthlem2  27053  fsumdvdscom  27169  musumsum  27176  chtub  27196  fsumvma  27197  perfectlem2  27214  dchrelbas3  27222  dchrelbasd  27223  dchrn0  27234  dchrptlem2  27249  lgsval2lem  27291  lgsdirnn0  27328  lgsdinn0  27329  2sqlem10  27412  dchrisumlem1  27473  dchrmusum2  27478  dchrvmasumlem2  27482  dchrvmasumlem3  27483  dchrvmasumiflem1  27485  dchrisum0flblem2  27493  dchrisum0flb  27494  dchrisum0lem1b  27499  dchrisum0lem2  27502  2vmadivsumlem  27524  chpdifbndlem1  27537  selberg3lem1  27541  selberg4lem1  27544  pntrsumbnd2  27551  pntrlog2bndlem2  27562  pntrlog2bndlem3  27563  pntrlog2bndlem5  27565  pntrlog2bndlem6  27567  pntibndlem2  27575  pntibndlem3  27576  pntlemn  27584  pntlemj  27587  pntlemi  27588  pntlemo  27591  pntleme  27592  pntlem3  27593  pntlemp  27594  ostth2lem1  27602  ostthlem1  27611  ostth2lem2  27618  ostth3  27622  nosupprefixmo  27684  noinfprefixmo  27685  noinfbnd1lem1  27707  noinfbnd1lem4  27710  noinfbnd2lem1  27714  noinfbnd2  27715  eqcuts3  27816  cofslts  27930  coinitslts  27931  leadds1  28001  addsass  28017  addbdaylem  28029  negsid  28053  mulscom  28151  addsdilem3  28165  addsdilem4  28166  mulsasslem3  28177  precsexlem8  28226  precsexlem9  28227  precsexlem11  28229  addonbday  28291  n0fincut  28367  onsfi  28368  bdayfinbndlem1  28479  bdayfinbnd  28481  tglowdim1i  28589  tglowdim2ln  28739  wlkonl1iedg  29752  wlkp1lem7  29766  wlkp1lem8  29767  crctcshwlkn0lem6  29903  eupth2eucrct  30307  eupth2lem3  30326  ubthlem1  30961  ubthlem2  30962  minvecolem3  30967  occllem  31394  pjhthlem1  31482  eqelbid  32564  fnfvor  32703  ofrco  32704  wrdt2ind  33034  mgccole1  33071  mgcmnt2  33074  dfmgc2  33077  fxpgaeq  33252  fxpsubm  33255  fxpsubg  33256  fxpsubrg  33257  elrgspnlem4  33328  elrgspnsubrunlem2  33331  0nellinds  33455  linds2eq  33466  elrspunidl  33513  prmidl  33525  mxidlmax  33550  ssmxidl  33559  1arithidomlem1  33628  1arithidom  33630  1arithufdlem3  33639  1arithufdlem4  33640  ply1dg1rt  33673  vietalem  33773  lbsdiflsp0  33820  fedgmullem1  33823  fedgmullem2  33824  extdg1id  33860  fldextrspunlsplem  33867  extdgfialglem2  33887  constrsscn  33934  constrconj  33939  zrhcntr  34173  ofcfeqd2  34295  inelpisys  34348  unelldsys  34352  ldgenpisyslem1  34357  mbfmcnvima  34449  signstfvneq0  34766  fsum2dsub  34801  hgt750lemc  34841  hgt750lemd  34842  hgt749d  34843  hgt750lemf  34847  bnj1379  35025  bnj1450  35245  revwlk  35366  subfacp1lem5  35425  cvmlift2lem10  35553  weiunfrlem  36705  weiunpo  36706  weiunso  36707  weiunfr  36708  weiunse  36709  unblimceq0lem  36825  unblimceq0  36826  unbdqndv2  36830  bj-ismoored  37478  lcmineqlem4  42530  dvle2  42570  aks4d1p9  42586  primrootlekpowne0  42603  aks6d1c1p3  42608  aks6d1c1p4  42609  aks6d1c1p5  42610  aks6d1c1  42614  hashscontpow  42620  aks6d1c2lem3  42624  sticksstones1  42644  aks6d1c6lem1  42668  aks6d1c6lem2  42669  aks6d1c6lem4  42671  aks6d1c7  42682  aks5lem3a  42687  unitscyglem1  42693  unitscyglem2  42694  unitscyglem3  42695  unitscyglem4  42696  exfinfldd  42701  fnwe2lem2  43509  aomclem4  43515  scottelrankd  44704  mnuop123d  44719  mnuprdlem1  44729  mnuprdlem2  44730  eliind  45532  rnmptbd2lem  45704  rnmptbdlem  45711  cvgcau  45945  limclner  46106  climisp  46201  climrescn  46203  climxrrelem  46204  climxrre  46205  liminflelimsuplem  46230  cncfshift  46329  cncfperiod  46334  fperdvper  46374  salunicl  46771  saldifcl  46774  meadjuni  46912  chnerlem1  47339  lubsscl  49462  glbsscl  49463  ipolub  49490  ipoglb  49493  ssccatid  49574  upciclem1  49668  oppcup3lem  49708  oppcthinendcALT  49943  setcthin  49967