Theorem rspcdva 3583

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2143  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080

This theorem is referenced by:  nvocnv  7281  knatar  7357  caofref  7707  caofinvl  7708  tfisi  7856  frxp2  8141  frxp3  8148  suppssov1  8194  suppssov2  8195  fpr3g  8283  fprresex  8308  tfrlem1  8363  tfrlem5  8367  coflton  8658  cofon1  8659  cofon2  8660  marypha1lem  9394  marypha1  9395  ordtypelem6  9486  ordtypelem7  9487  wemaplem2  9510  oemapvali  9654  cantnflem1c  9657  ttrcltr  9686  ttrclss  9690  dmttrcl  9691  rnttrcl  9692  ttrclselem2  9696  scottelrankd  9874  infxpenlem  9998  acni  10030  dfac9  10121  dfac12lem2  10129  sornom  10262  fin1ai  10278  fin2i  10280  fin23lem11  10302  isfin2-2  10304  fin23lem17  10323  fin23lem39  10335  fin1a2lem13  10397  hsmexlem4  10414  ttukeylem5  10498  ttukeylem6  10499  canth4  10633  pwfseqlem5  10649  winalim2  10682  wununi  10692  wunpw  10693  dedekind  11374  zsupss  12962  uzwo3  12968  seqcl2  14058  seqcl  14060  seqf  14061  seqfveq2  14062  seqfveq  14064  seqshft2  14066  monoord  14070  monoord2  14071  sermono  14072  seqsplit  14073  seqcaopr3  14075  seqid  14085  seqid2  14086  seqhomo  14087  seqz  14088  discr1  14277  discr  14278  hashbclem  14491  wrdind  14761  limsupgre  15534  climi  15563  rlimi  15566  rlimclim1  15598  rlimclim  15599  climrlim2  15600  rlimcn1  15641  climcn1  15645  isercoll2  15722  caucvgrlem  15726  caucvgb  15733  iseraltlem2  15736  iseraltlem3  15737  fsumm1  15804  fsum1p  15806  fsumcom2  15827  fsumge1  15851  telfsumo  15856  telfsumo2  15857  fsumparts  15860  o1fsum  15867  isum1p  15897  isumnn0nn  15898  isumrpcl  15899  climcndslem1  15905  climcndslem2  15906  climcnds  15907  cvgrat  15939  mertenslem1  15940  mertens  15942  fprodm1  16023  fprod1p  16024  fprodcom2  16040  prmind2  16744  pcmpt2  16954  prmpwdvds  16965  prmreclem4  16980  prmreclem5  16981  vdwlem1  17042  vdwlem2  17043  vdwlem9  17050  vdwlem10  17051  rami  17076  ramcl  17090  prmodvdslcmf  17108  prmgaplcmlem1  17112  cshwsidrepsw  17154  prdsbasprj  17526  isacs2  17710  acsfiel  17711  catidex  17731  iscatd2  17738  catlid  17740  catrid  17741  subcidcl  17902  funcid  17928  yonedalem4c  18334  yonffthlem  18339  isdrs2  18363  luble  18414  glble  18427  joinle  18441  meetle  18455  poslubmo  18466  posglbmo  18467  acsdrsel  18600  isacs4lem  18601  isacs5lem  18602  acsdrscl  18603  acsficl  18604  chnltm1  18666  chnub  18679  lidrideqd  18728  grpinvalem  18732  grpinva  18733  mndind  18888  grpidd2  19045  mulgsubcl  19155  issubg4  19213  ghmf1  19317  fislw  19696  efgsdmi  19803  efgsrel  19805  gexexlem  19923  gsumzaddlem  19992  gsummhm2  20010  dprdcntz  20081  dprddisj  20082  dprdss  20102  dprd2dlem2  20113  dprd2da  20115  dpjrid  20135  ablfac1eu  20146  pgpfac1lem1  20147  pgpfaclem2  20155  lringuplu  20630  issrngd  20939  islbs2  21259  lbsextlem4  21266  prmidl  21446  prmirredlem  21603  psgndiflemB  21731  frlmphl  21912  mplsubglem  22129  mpllsslem  22130  subrgasclcl  22199  mplind  22202  evlslem1  22214  ply1scleq  22446  mdetralt  22746  mdetunilem1  22750  lmcvg  23400  iscncl  23407  lmff  23439  cnrmi  23498  cmpcov  23527  fiuncmp  23542  hauscmplem  23544  1stcfb  23583  1stcelcls  23599  restnlly  23620  islly2  23622  lly1stc  23634  kgeni  23675  ptpjpre1  23709  ptbasfi  23719  ptpjopn  23750  dfac14  23756  txtube  23778  cnmpt11  23801  cnmpt21  23809  cnmptkp  23818  cnmptk1p  23823  qtopomap  23856  qtopcmap  23857  flimcf  24120  fclscf  24163  flfcntr  24181  ptcmplem3  24192  tgpt0  24257  tsmsi  24272  tsmsxplem2  24292  tsmsxp  24293  isucn2  24416  ucnima  24418  ucncn  24422  cfiluweak  24432  cuspcvg  24438  imasdsf1olem  24511  lpbl  24641  comet  24651  cfilucfil  24697  cnheiborlem  25094  cnheibor  25095  bndth  25098  nmoleub2lem2  25256  nmoleub3  25259  ipcau2  25374  tcphcphlem1  25375  tcphcphlem2  25376  lmmcvg  25401  cmetcaulem  25428  iscmet3lem1  25431  iscmet3lem2  25432  pjthlem1  25577  pjthlem2  25578  ivthlem1  25591  ivthlem2  25592  ivthlem3  25593  ivth2  25595  ivthle  25596  ivthle2  25597  ivthicc  25598  ovoliunlem1  25642  ovolshftlem1  25649  ovolscalem1  25653  ovolicc2lem3  25659  ovolicc2lem4  25660  ovolicc2  25662  volsup  25696  dyadmbl  25740  vitalilem2  25749  vitalilem3  25750  mbfdm  25766  ismbf3d  25794  cncombf  25798  itg2seq  25882  itg2monolem2  25891  itg2monolem3  25892  itg2mono  25893  iblitg  25908  itgconst  25959  itgfsum  25967  limcvallem  26011  cnlimci  26029  cnmptlimc  26030  dvferm1lem  26124  dvferm1  26125  dvferm2lem  26126  dvferm2  26127  dvlipcn  26134  dvle  26147  lhop1lem  26153  dvfsumge  26162  dvfsumlem2  26167  dvfsumlem3  26168  ftc1a  26177  ftc1lem4  26179  itgsubstlem  26188  mdeglt  26203  deg1lt  26235  ply1divex  26275  fta1glem2  26307  fta1g  26308  plyco0  26330  plyeq0lem  26348  dgrcolem2  26412  plydivlem4  26438  plydivex  26439  fta1lem  26449  vieta1lem2  26453  vieta1  26454  tayl0  26506  ulmi  26530  ulmdvlem1  26544  ulmdvlem3  26546  ulmdv  26547  mtest  26548  pserulm  26566  efif1olem4  26691  rlimcnp  27111  rlimcnp2  27112  xrlimcnp  27114  scvxcvx  27131  lgamgulmlem5  27178  lgambdd  27182  lgamcvglem  27185  wilthlem2  27214  fsumdvdscom  27330  musumsum  27337  chtub  27357  fsumvma  27358  perfectlem2  27375  dchrelbas3  27383  dchrelbasd  27384  dchrn0  27395  dchrptlem2  27410  lgsval2lem  27452  lgsdirnn0  27489  lgsdinn0  27490  2sqlem10  27573  dchrisumlem1  27634  dchrmusum2  27639  dchrvmasumlem2  27643  dchrvmasumlem3  27644  dchrvmasumiflem1  27646  dchrisum0flblem2  27654  dchrisum0flb  27655  dchrisum0lem1b  27660  dchrisum0lem2  27663  2vmadivsumlem  27685  chpdifbndlem1  27698  selberg3lem1  27702  selberg4lem1  27705  pntrsumbnd2  27712  pntrlog2bndlem2  27723  pntrlog2bndlem3  27724  pntrlog2bndlem5  27726  pntrlog2bndlem6  27728  pntibndlem2  27736  pntibndlem3  27737  pntlemn  27745  pntlemj  27748  pntlemi  27749  pntlemo  27752  pntleme  27753  pntlem3  27754  pntlemp  27755  ostth2lem1  27763  ostthlem1  27772  ostth2lem2  27779  ostth3  27783  nosupprefixmo  27845  noinfprefixmo  27846  noinfbnd1lem1  27868  noinfbnd1lem4  27871  noinfbnd2lem1  27875  noinfbnd2  27876  eqcuts3  27978  cofslts  28092  coinitslts  28093  leadds1  28163  addsass  28179  addbdaylem  28191  negsid  28215  mulscom  28313  addsdilem3  28327  addsdilem4  28328  mulsasslem3  28339  precsexlem8  28388  precsexlem9  28389  precsexlem11  28391  addonbday  28453  n0fincut  28529  onsfi  28530  bdayfinbndlem1  28641  bdayfinbnd  28643  tglowdim1i  28751  tglowdim2ln  28906  wlkonl1iedg  29994  wlkp1lem7  30008  wlkp1lem8  30009  crctcshwlkn0lem6  30145  eupth2eucrct  30549  eupth2lem3  30568  ubthlem1  31203  ubthlem2  31204  minvecolem3  31209  occllem  31636  pjhthlem1  31724  eqelbid  32802  fnfvor  32935  ofrco  32936  wrdt2ind  33254  mgccole1  33291  mgcmnt2  33294  dfmgc2  33297  fxpgaeq  33470  fxpsubm  33473  fxpsubg  33474  fxpsubrg  33475  elrgspnlem4  33546  elrgspnsubrunlem2  33549  0nellinds  33666  linds2eq  33675  elrspunidl  33717  mxidlmax  33729  ssmxidl  33738  1arithidomlem1  33806  1arithidom  33808  1arithufdlem3  33817  1arithufdlem4  33818  ply1dg1rt  33851  vietalem  33950  lbsdiflsp0  33997  fedgmullem1  34000  fedgmullem2  34001  extdg1id  34037  fldextrspunlsplem  34044  extdgfialglem2  34064  constrsscn  34111  constrconj  34116  zrhcntr  34350  ofcfeqd2  34472  inelpisys  34525  unelldsys  34529  ldgenpisyslem1  34534  mbfmcnvima  34626  signstfvneq0  34940  fsum2dsub  34975  hgt750lemc  35015  hgt750lemd  35016  hgt749d  35017  hgt750lemf  35021  bnj1379  35199  bnj1450  35419  revwlk  35598  subfacp1lem5  35657  cvmlift2lem10  35785  nmulprop  36663  nmulcom  36667  weiunfrlem  36956  weiunpo  36957  weiunso  36958  weiunfr  36959  weiunse  36960  unblimceq0lem  37076  unblimceq0  37077  unbdqndv2  37081  bj-ismoored  37730  lcmineqlem4  42780  dvle2  42820  aks4d1p9  42836  primrootlekpowne0  42853  aks6d1c1p3  42858  aks6d1c1p4  42859  aks6d1c1p5  42860  aks6d1c1  42864  hashscontpow  42870  aks6d1c2lem3  42874  sticksstones1  42894  aks6d1c6lem1  42918  aks6d1c6lem2  42919  aks6d1c6lem4  42921  aks6d1c7  42932  aks5lem3a  42937  unitscyglem1  42943  unitscyglem2  42944  unitscyglem3  42945  unitscyglem4  42946  exfinfldd  42951  fnwe2lem2  43761  aomclem4  43767  mnuop123d  44955  mnuprdlem1  44965  mnuprdlem2  44966  eliind  45774  rnmptbd2lem  45946  rnmptbdlem  45953  cvgcau  46187  limclner  46348  climisp  46443  climrescn  46445  climxrrelem  46446  climxrre  46447  liminflelimsuplem  46472  cncfshift  46571  cncfperiod  46576  fperdvper  46616  fourierdlem48  46851  salunicl  47013  saldifcl  47016  meadjuni  47154  chnerlem1  47581  lubsscl  49721  glbsscl  49722  ipolub  49749  ipoglb  49752  ssccatid  49833  upciclem1  49927  oppcup3lem  49967  oppcthinendcALT  50202  setcthin  50226