Theorem rspcdva 3584

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2146  ∀wral 3081

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082

This theorem is used by:  nvocnv  7285  knatar  7363  caofref  7711  caofinvl  7712  tfisi  7857  frxp2  8142  frxp3  8149  suppssov1  8195  suppssov2  8196  fpr3g  8284  fprresex  8309  tfrlem1  8364  tfrlem5  8368  coflton  8659  cofon1  8660  cofon2  8661  marypha1lem  9396  marypha1  9397  ordtypelem6  9488  ordtypelem7  9489  wemaplem2  9512  oemapvali  9656  cantnflem1c  9659  ttrcltr  9688  ttrclss  9692  dmttrcl  9693  rnttrcl  9694  ttrclselem2  9698  scottelrankd  9880  infxpenlem  10009  acni  10041  dfac9  10132  dfac12lem2  10140  sornom  10272  fin1ai  10288  fin2i  10290  fin23lem11  10312  isfin2-2  10314  fin23lem17  10333  fin23lem39  10345  fin1a2lem13  10407  hsmexlem4  10424  ttukeylem5  10508  ttukeylem6  10509  canth4  10643  pwfseqlem5  10659  winalim2  10692  wununi  10702  wunpw  10703  dedekind  11384  zsupss  12972  uzwo3  12978  seqcl2  14069  seqcl  14071  seqf  14072  seqfveq2  14073  seqfveq  14075  seqshft2  14077  monoord  14081  monoord2  14082  sermono  14083  seqsplit  14084  seqcaopr3  14086  seqid  14096  seqid2  14097  seqhomo  14098  seqz  14099  discr1  14288  discr  14289  hashbclem  14502  wrdind  14776  limsupgre  15551  climi  15580  rlimi  15583  rlimclim1  15615  rlimclim  15616  climrlim2  15617  rlimcn1  15658  climcn1  15662  isercoll2  15739  caucvgrlem  15743  caucvgb  15750  iseraltlem2  15753  iseraltlem3  15754  fsumm1  15820  fsum1p  15822  fsumcom2  15843  fsumge1  15867  telfsumo  15872  telfsumo2  15873  fsumparts  15876  o1fsum  15883  isum1p  15913  isumnn0nn  15914  isumrpcl  15915  climcndslem1  15921  climcndslem2  15922  climcnds  15923  cvgrat  15955  mertenslem1  15956  mertens  15958  fprodm1  16039  fprod1p  16040  fprodcom2  16056  prmind2  16760  pcmpt2  16970  prmpwdvds  16981  prmreclem4  16996  prmreclem5  16997  vdwlem1  17058  vdwlem2  17059  vdwlem9  17066  vdwlem10  17067  rami  17092  ramcl  17106  prmodvdslcmf  17124  prmgaplcmlem1  17128  cshwsidrepsw  17170  prdsbasprj  17542  isacs2  17726  acsfiel  17727  catidex  17747  iscatd2  17754  catlid  17756  catrid  17757  subcidcl  17918  funcid  17944  yonedalem4c  18350  yonffthlem  18355  isdrs2  18379  luble  18430  glble  18443  joinle  18457  meetle  18471  poslubmo  18482  posglbmo  18483  acsdrsel  18616  isacs4lem  18617  isacs5lem  18618  acsdrscl  18619  acsficl  18620  chnltm1  18682  chnub  18695  lidrideqd  18745  grpinvalem  18749  grpinva  18750  mndind  18910  grpidd2  19067  mulgsubcl  19177  issubg4  19235  ghmf1  19339  fislw  19718  efgsdmi  19825  efgsrel  19827  gexexlem  19945  gsumzaddlem  20014  gsummhm2  20032  dprdcntz  20103  dprddisj  20104  dprdss  20124  dprd2dlem2  20135  dprd2da  20137  dpjrid  20157  ablfac1eu  20168  pgpfac1lem1  20169  pgpfaclem2  20177  lringuplu  20672  issrngd  20987  islbs2  21307  lbsextlem4  21314  prmidl  21494  prmirredlem  21651  psgndiflemB  21779  frlmphl  21960  mplsubglem  22177  mpllsslem  22178  subrgasclcl  22247  mplind  22250  evlslem1  22262  ply1scleq  22494  mdetralt  22794  mdetunilem1  22798  lmcvg  23448  iscncl  23455  lmff  23487  cnrmi  23546  cmpcov  23575  fiuncmp  23590  hauscmplem  23592  1stcfb  23631  1stcelcls  23647  restnlly  23668  islly2  23670  lly1stc  23682  kgeni  23723  ptpjpre1  23757  ptbasfi  23767  ptpjopn  23798  dfac14  23804  txtube  23826  cnmpt11  23849  cnmpt21  23857  cnmptkp  23866  cnmptk1p  23871  qtopomap  23904  qtopcmap  23905  flimcf  24168  fclscf  24211  flfcntr  24229  ptcmplem3  24240  tgpt0  24305  tsmsi  24320  tsmsxplem2  24340  tsmsxp  24341  isucn2  24464  ucnima  24466  ucncn  24470  cfiluweak  24480  cuspcvg  24486  imasdsf1olem  24559  lpbl  24689  comet  24699  cfilucfil  24745  cnheiborlem  25142  cnheibor  25143  bndth  25146  nmoleub2lem2  25304  nmoleub3  25307  ipcau2  25422  tcphcphlem1  25423  tcphcphlem2  25424  lmmcvg  25449  cmetcaulem  25476  iscmet3lem1  25479  iscmet3lem2  25480  pjthlem1  25625  pjthlem2  25626  ivthlem1  25639  ivthlem2  25640  ivthlem3  25641  ivth2  25643  ivthle  25644  ivthle2  25645  ivthicc  25646  ovoliunlem1  25690  ovolshftlem1  25697  ovolscalem1  25701  ovolicc2lem3  25707  ovolicc2lem4  25708  ovolicc2  25710  volsup  25744  dyadmbl  25788  vitalilem2  25797  vitalilem3  25798  mbfdm  25814  ismbf3d  25842  cncombf  25846  itg2seq  25930  itg2monolem2  25939  itg2monolem3  25940  itg2mono  25941  iblitg  25956  itgconst  26007  itgfsum  26015  limcvallem  26059  cnlimci  26077  cnmptlimc  26078  dvferm1lem  26172  dvferm1  26173  dvferm2lem  26174  dvferm2  26175  dvlipcn  26182  dvle  26195  lhop1lem  26201  dvfsumge  26210  dvfsumlem2  26215  dvfsumlem3  26216  ftc1a  26225  ftc1lem4  26227  itgsubstlem  26236  mdeglt  26251  deg1lt  26283  ply1divex  26323  fta1glem2  26355  fta1g  26356  plyco0  26378  plyeq0lem  26396  dgrcolem2  26460  plydivlem4  26486  plydivex  26487  fta1lem  26497  vieta1lem2  26501  vieta1  26502  tayl0  26554  ulmi  26578  ulmdvlem1  26592  ulmdvlem3  26594  ulmdv  26595  mtest  26596  pserulm  26614  efif1olem4  26739  rlimcnp  27159  rlimcnp2  27160  xrlimcnp  27162  scvxcvx  27179  lgamgulmlem5  27226  lgambdd  27230  lgamcvglem  27233  wilthlem2  27262  fsumdvdscom  27378  musumsum  27385  chtub  27405  fsumvma  27406  perfectlem2  27423  dchrelbas3  27431  dchrelbasd  27432  dchrn0  27443  dchrptlem2  27458  lgsval2lem  27500  lgsdirnn0  27537  lgsdinn0  27538  2sqlem10  27621  dchrisumlem1  27682  dchrmusum2  27687  dchrvmasumlem2  27691  dchrvmasumlem3  27692  dchrvmasumiflem1  27694  dchrisum0flblem2  27702  dchrisum0flb  27703  dchrisum0lem1b  27708  dchrisum0lem2  27711  2vmadivsumlem  27733  chpdifbndlem1  27746  selberg3lem1  27750  selberg4lem1  27753  pntrsumbnd2  27760  pntrlog2bndlem2  27771  pntrlog2bndlem3  27772  pntrlog2bndlem5  27774  pntrlog2bndlem6  27776  pntibndlem2  27784  pntibndlem3  27785  pntlemn  27793  pntlemj  27796  pntlemi  27797  pntlemo  27800  pntleme  27801  pntlem3  27802  pntlemp  27803  ostth2lem1  27811  ostthlem1  27820  ostth2lem2  27827  ostth3  27831  nosupprefixmo  27893  noinfprefixmo  27894  noinfbnd1lem1  27916  noinfbnd1lem4  27919  noinfbnd2lem1  27923  noinfbnd2  27924  eqcuts3  28026  cofslts  28140  coinitslts  28141  leadds1  28211  addsass  28227  addbdaylem  28239  negsid  28263  mulscom  28361  addsdilem3  28375  addsdilem4  28376  mulsasslem3  28387  precsexlem8  28436  precsexlem9  28437  precsexlem11  28439  addonbday  28501  n0fincut  28577  onsfi  28578  bdayfinbndlem1  28689  bdayfinbnd  28691  tglowdim1i  28799  tglowdim2ln  28954  wlkonl1iedg  30042  wlkp1lem7  30056  wlkp1lem8  30057  crctcshwlkn0lem6  30193  eupth2eucrct  30597  eupth2lem3  30616  ubthlem1  31251  ubthlem2  31252  minvecolem3  31257  occllem  31684  pjhthlem1  31772  eqelbid  32850  fnfvor  32983  ofrco  32984  wrdt2ind  33298  mgccole1  33333  mgcmnt2  33336  dfmgc2  33339  fxpgaeq  33512  fxpsubm  33515  fxpsubg  33516  fxpsubrg  33517  elrgspnlem4  33588  elrgspnsubrunlem2  33591  0nellinds  33708  linds2eq  33717  elrspunidl  33759  mxidlmax  33771  ssmxidl  33780  1arithidomlem1  33848  1arithidom  33850  1arithufdlem3  33859  1arithufdlem4  33860  ply1dg1rt  33893  vietalem  33992  lbsdiflsp0  34039  fedgmullem1  34042  fedgmullem2  34043  extdg1id  34079  fldextrspunlsplem  34086  extdgfialglem2  34106  constrsscn  34153  constrconj  34158  zrhcntr  34392  ofcfeqd2  34514  inelpisys  34568  unelldsys  34572  ldgenpisyslem1  34577  mbfmcnvima  34669  signstfvneq0  34983  fsum2dsub  35018  hgt750lemc  35058  hgt750lemd  35059  hgt749d  35060  hgt750lemf  35064  bnj1379  35242  bnj1450  35462  revwlk  35630  subfacp1lem5  35689  cvmlift2lem10  35817  nmulprop  36695  nmulcom  36699  nadddilem1  36725  nadddilem3  36727  weiunfrlem  37008  weiunpo  37009  weiunso  37010  weiunfr  37011  weiunse  37012  unblimceq0lem  37128  unblimceq0  37129  unbdqndv2  37133  bj-ismoored  37782  lcmineqlem4  42832  dvle2  42872  aks4d1p9  42888  primrootlekpowne0  42905  aks6d1c1p3  42910  aks6d1c1p4  42911  aks6d1c1p5  42912  aks6d1c1  42916  hashscontpow  42922  aks6d1c2lem3  42926  sticksstones1  42946  aks6d1c6lem1  42970  aks6d1c6lem2  42971  aks6d1c6lem4  42973  aks6d1c7  42984  aks5lem3a  42989  unitscyglem1  42995  unitscyglem2  42996  unitscyglem3  42997  unitscyglem4  42998  exfinfldd  43003  fnwe2lem2  43811  aomclem4  43817  mnuop123d  45005  mnuprdlem1  45015  mnuprdlem2  45016  eliind  45824  rnmptbd2lem  45996  rnmptbdlem  46003  cvgcau  46237  limclner  46398  climisp  46493  climrescn  46495  climxrrelem  46496  climxrre  46497  liminflelimsuplem  46522  cncfshift  46621  cncfperiod  46626  fperdvper  46666  fourierdlem48  46901  salunicl  47063  saldifcl  47066  meadjuni  47204  chnerlem1  47631  lubsscl  49771  glbsscl  49772  ipolub  49799  ipoglb  49802  ssccatid  49883  upciclem1  49977  oppcup3lem  50017  oppcthinendcALT  50252  setcthin  50276