Theorem rspcdva 3591

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086

This theorem is referenced by:  nvocnv  7277  knatar  7353  caofref  7703  caofinvl  7704  tfisi  7851  frxp2  8136  frxp3  8143  suppssov1  8189  suppssov2  8190  fpr3g  8278  fprresex  8303  tfrlem1  8358  tfrlem5  8362  coflton  8653  cofon1  8654  cofon2  8655  marypha1lem  9389  marypha1  9390  ordtypelem6  9481  ordtypelem7  9482  wemaplem2  9505  oemapvali  9649  cantnflem1c  9652  ttrcltr  9681  ttrclss  9685  dmttrcl  9686  rnttrcl  9687  ttrclselem2  9691  scottelrankd  9869  infxpenlem  9993  acni  10025  dfac9  10116  dfac12lem2  10124  sornom  10257  fin1ai  10273  fin2i  10275  fin23lem11  10297  isfin2-2  10299  fin23lem17  10318  fin23lem39  10330  fin1a2lem13  10392  hsmexlem4  10409  ttukeylem5  10493  ttukeylem6  10494  canth4  10628  pwfseqlem5  10644  winalim2  10677  wununi  10687  wunpw  10688  dedekind  11369  zsupss  12957  uzwo3  12963  seqcl2  14052  seqcl  14054  seqf  14055  seqfveq2  14056  seqfveq  14058  seqshft2  14060  monoord  14064  monoord2  14065  sermono  14066  seqsplit  14067  seqcaopr3  14069  seqid  14079  seqid2  14080  seqhomo  14081  seqz  14082  discr1  14271  discr  14272  hashbclem  14485  wrdind  14755  limsupgre  15528  climi  15557  rlimi  15560  rlimclim1  15592  rlimclim  15593  climrlim2  15594  rlimcn1  15635  climcn1  15639  isercoll2  15716  caucvgrlem  15720  caucvgb  15727  iseraltlem2  15730  iseraltlem3  15731  fsumm1  15798  fsum1p  15800  fsumcom2  15821  fsumge1  15845  telfsumo  15850  telfsumo2  15851  fsumparts  15854  o1fsum  15861  isum1p  15891  isumnn0nn  15892  isumrpcl  15893  climcndslem1  15899  climcndslem2  15900  climcnds  15901  cvgrat  15933  mertenslem1  15934  mertens  15936  fprodm1  16017  fprod1p  16018  fprodcom2  16034  prmind2  16739  pcmpt2  16949  prmpwdvds  16960  prmreclem4  16975  prmreclem5  16976  vdwlem1  17037  vdwlem2  17038  vdwlem9  17045  vdwlem10  17046  rami  17071  ramcl  17085  prmodvdslcmf  17103  prmgaplcmlem1  17107  cshwsidrepsw  17149  prdsbasprj  17521  isacs2  17705  acsfiel  17706  catidex  17726  iscatd2  17733  catlid  17735  catrid  17736  subcidcl  17897  funcid  17923  yonedalem4c  18329  yonffthlem  18334  isdrs2  18358  luble  18409  glble  18422  joinle  18436  meetle  18450  poslubmo  18461  posglbmo  18462  acsdrsel  18595  isacs4lem  18596  isacs5lem  18597  acsdrscl  18598  acsficl  18599  chnltm1  18661  chnub  18674  lidrideqd  18723  grpinvalem  18727  grpinva  18728  mndind  18883  grpidd2  19040  mulgsubcl  19150  issubg4  19208  ghmf1  19312  fislw  19691  efgsdmi  19798  efgsrel  19800  gexexlem  19918  gsumzaddlem  19987  gsummhm2  20005  dprdcntz  20076  dprddisj  20077  dprdss  20097  dprd2dlem2  20108  dprd2da  20110  dpjrid  20130  ablfac1eu  20141  pgpfac1lem1  20142  pgpfaclem2  20150  lringuplu  20625  issrngd  20932  islbs2  21252  lbsextlem4  21259  prmidl  21432  prmirredlem  21587  psgndiflemB  21715  frlmphl  21896  mplsubglem  22113  mpllsslem  22114  subrgasclcl  22183  mplind  22186  evlslem1  22198  ply1scleq  22430  mdetralt  22730  mdetunilem1  22734  lmcvg  23384  iscncl  23391  lmff  23423  cnrmi  23482  cmpcov  23511  fiuncmp  23526  hauscmplem  23528  1stcfb  23567  1stcelcls  23583  restnlly  23604  islly2  23606  lly1stc  23618  kgeni  23659  ptpjpre1  23693  ptbasfi  23703  ptpjopn  23734  dfac14  23740  txtube  23762  cnmpt11  23785  cnmpt21  23793  cnmptkp  23802  cnmptk1p  23807  qtopomap  23840  qtopcmap  23841  flimcf  24104  fclscf  24147  flfcntr  24165  ptcmplem3  24176  tgpt0  24241  tsmsi  24256  tsmsxplem2  24276  tsmsxp  24277  isucn2  24400  ucnima  24402  ucncn  24406  cfiluweak  24416  cuspcvg  24422  imasdsf1olem  24495  lpbl  24625  comet  24635  cfilucfil  24681  cnheiborlem  25078  cnheibor  25079  bndth  25082  nmoleub2lem2  25240  nmoleub3  25243  ipcau2  25358  tcphcphlem1  25359  tcphcphlem2  25360  lmmcvg  25385  cmetcaulem  25412  iscmet3lem1  25415  iscmet3lem2  25416  pjthlem1  25561  pjthlem2  25562  ivthlem1  25575  ivthlem2  25576  ivthlem3  25577  ivth2  25579  ivthle  25580  ivthle2  25581  ivthicc  25582  ovoliunlem1  25626  ovolshftlem1  25633  ovolscalem1  25637  ovolicc2lem3  25643  ovolicc2lem4  25644  ovolicc2  25646  volsup  25680  dyadmbl  25724  vitalilem2  25733  vitalilem3  25734  mbfdm  25750  ismbf3d  25778  cncombf  25782  itg2seq  25866  itg2monolem2  25875  itg2monolem3  25876  itg2mono  25877  iblitg  25892  itgconst  25943  itgfsum  25951  limcvallem  25995  cnlimci  26013  cnmptlimc  26014  dvferm1lem  26108  dvferm1  26109  dvferm2lem  26110  dvferm2  26111  dvlipcn  26118  dvle  26131  lhop1lem  26137  dvfsumge  26146  dvfsumlem2  26151  dvfsumlem3  26152  ftc1a  26161  ftc1lem4  26163  itgsubstlem  26172  mdeglt  26187  deg1lt  26219  ply1divex  26259  fta1glem2  26291  fta1g  26292  plyco0  26314  plyeq0lem  26332  dgrcolem2  26396  plydivlem4  26422  plydivex  26423  fta1lem  26433  vieta1lem2  26437  vieta1  26438  tayl0  26487  ulmi  26511  ulmdvlem1  26525  ulmdvlem3  26527  ulmdv  26528  mtest  26529  pserulm  26547  efif1olem4  26672  rlimcnp  27092  rlimcnp2  27093  xrlimcnp  27095  scvxcvx  27112  lgamgulmlem5  27159  lgambdd  27163  lgamcvglem  27166  wilthlem2  27195  fsumdvdscom  27311  musumsum  27318  chtub  27338  fsumvma  27339  perfectlem2  27356  dchrelbas3  27364  dchrelbasd  27365  dchrn0  27376  dchrptlem2  27391  lgsval2lem  27433  lgsdirnn0  27470  lgsdinn0  27471  2sqlem10  27554  dchrisumlem1  27615  dchrmusum2  27620  dchrvmasumlem2  27624  dchrvmasumlem3  27625  dchrvmasumiflem1  27627  dchrisum0flblem2  27635  dchrisum0flb  27636  dchrisum0lem1b  27641  dchrisum0lem2  27644  2vmadivsumlem  27666  chpdifbndlem1  27679  selberg3lem1  27683  selberg4lem1  27686  pntrsumbnd2  27693  pntrlog2bndlem2  27704  pntrlog2bndlem3  27705  pntrlog2bndlem5  27707  pntrlog2bndlem6  27709  pntibndlem2  27717  pntibndlem3  27718  pntlemn  27726  pntlemj  27729  pntlemi  27730  pntlemo  27733  pntleme  27734  pntlem3  27735  pntlemp  27736  ostth2lem1  27744  ostthlem1  27753  ostth2lem2  27760  ostth3  27764  nosupprefixmo  27826  noinfprefixmo  27827  noinfbnd1lem1  27849  noinfbnd1lem4  27852  noinfbnd2lem1  27856  noinfbnd2  27857  eqcuts3  27959  cofslts  28073  coinitslts  28074  leadds1  28144  addsass  28160  addbdaylem  28172  negsid  28196  mulscom  28294  addsdilem3  28308  addsdilem4  28309  mulsasslem3  28320  precsexlem8  28369  precsexlem9  28370  precsexlem11  28372  addonbday  28434  n0fincut  28510  onsfi  28511  bdayfinbndlem1  28622  bdayfinbnd  28624  tglowdim1i  28732  tglowdim2ln  28883  wlkonl1iedg  29950  wlkp1lem7  29964  wlkp1lem8  29965  crctcshwlkn0lem6  30101  eupth2eucrct  30505  eupth2lem3  30524  ubthlem1  31159  ubthlem2  31160  minvecolem3  31165  occllem  31592  pjhthlem1  31680  eqelbid  32758  fnfvor  32891  ofrco  32892  wrdt2ind  33210  mgccole1  33247  mgcmnt2  33250  dfmgc2  33253  fxpgaeq  33426  fxpsubm  33429  fxpsubg  33430  fxpsubrg  33431  elrgspnlem4  33502  elrgspnsubrunlem2  33505  0nellinds  33624  linds2eq  33634  elrspunidl  33676  mxidlmax  33689  ssmxidl  33698  1arithidomlem1  33766  1arithidom  33768  1arithufdlem3  33777  1arithufdlem4  33778  ply1dg1rt  33811  vietalem  33910  lbsdiflsp0  33957  fedgmullem1  33960  fedgmullem2  33961  extdg1id  33997  fldextrspunlsplem  34004  extdgfialglem2  34024  constrsscn  34071  constrconj  34076  zrhcntr  34310  ofcfeqd2  34432  inelpisys  34485  unelldsys  34489  ldgenpisyslem1  34494  mbfmcnvima  34586  signstfvneq0  34900  fsum2dsub  34935  hgt750lemc  34975  hgt750lemd  34976  hgt749d  34977  hgt750lemf  34981  bnj1379  35159  bnj1450  35379  revwlk  35512  subfacp1lem5  35571  cvmlift2lem10  35699  nmulprop  36577  nmulcom  36581  weiunfrlem  36860  weiunpo  36861  weiunso  36862  weiunfr  36863  weiunse  36864  unblimceq0lem  36980  unblimceq0  36981  unbdqndv2  36985  bj-ismoored  37632  lcmineqlem4  42684  dvle2  42724  aks4d1p9  42740  primrootlekpowne0  42757  aks6d1c1p3  42762  aks6d1c1p4  42763  aks6d1c1p5  42764  aks6d1c1  42768  hashscontpow  42774  aks6d1c2lem3  42778  sticksstones1  42798  aks6d1c6lem1  42822  aks6d1c6lem2  42823  aks6d1c6lem4  42825  aks6d1c7  42836  aks5lem3a  42841  unitscyglem1  42847  unitscyglem2  42848  unitscyglem3  42849  unitscyglem4  42850  exfinfldd  42855  fnwe2lem2  43663  aomclem4  43669  mnuop123d  44857  mnuprdlem1  44867  mnuprdlem2  44868  eliind  45676  rnmptbd2lem  45848  rnmptbdlem  45855  cvgcau  46089  limclner  46250  climisp  46345  climrescn  46347  climxrrelem  46348  climxrre  46349  liminflelimsuplem  46374  cncfshift  46473  cncfperiod  46478  fperdvper  46518  fourierdlem48  46753  salunicl  46915  saldifcl  46918  meadjuni  47056  chnerlem1  47483  lubsscl  49616  glbsscl  49617  ipolub  49644  ipoglb  49647  ssccatid  49728  upciclem1  49822  oppcup3lem  49862  oppcthinendcALT  50097  setcthin  50121