Theorem rspcdva 3598

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∀wral 3046

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3047

This theorem is referenced by:  nvocnv  7263  knatar  7339  caofref  7691  caofinvl  7692  tfisi  7843  frxp2  8132  frxp3  8139  suppssov1  8185  suppssov2  8186  fpr3g  8273  fprresex  8298  tfrlem1  8353  tfrlem5  8357  coflton  8646  cofon1  8647  cofon2  8648  marypha1lem  9402  marypha1  9403  ordtypelem6  9494  ordtypelem7  9495  wemaplem2  9518  oemapvali  9655  cantnflem1c  9658  ttrcltr  9687  ttrclss  9691  dmttrcl  9692  rnttrcl  9693  ttrclselem2  9697  infxpenlem  9984  acni  10016  dfac9  10108  dfac12lem2  10116  sornom  10248  fin1ai  10264  fin2i  10266  fin23lem11  10288  isfin2-2  10290  fin23lem17  10309  fin23lem39  10321  fin1a2lem13  10383  hsmexlem4  10400  ttukeylem5  10484  ttukeylem6  10485  canth4  10618  pwfseqlem5  10634  winalim2  10667  wununi  10677  wunpw  10678  dedekind  11355  zsupss  12910  uzwo3  12916  seqcl2  13995  seqcl  13997  seqf  13998  seqfveq2  13999  seqfveq  14001  seqshft2  14003  monoord  14007  monoord2  14008  sermono  14009  seqsplit  14010  seqcaopr3  14012  seqid  14022  seqid2  14023  seqhomo  14024  seqz  14025  discr1  14214  discr  14215  hashbclem  14427  wrdind  14697  limsupgre  15454  climi  15483  rlimi  15486  rlimclim1  15518  rlimclim  15519  climrlim2  15520  rlimcn1  15561  climcn1  15565  isercoll2  15642  caucvgrlem  15646  caucvgb  15653  iseraltlem2  15656  iseraltlem3  15657  fsumm1  15724  fsum1p  15726  fsumcom2  15747  fsumge1  15770  telfsumo  15775  telfsumo2  15776  fsumparts  15779  o1fsum  15786  isum1p  15814  isumnn0nn  15815  isumrpcl  15816  climcndslem1  15822  climcndslem2  15823  climcnds  15824  cvgrat  15856  mertenslem1  15857  mertens  15859  fprodm1  15940  fprod1p  15941  fprodcom2  15957  prmind2  16661  pcmpt2  16870  prmpwdvds  16881  prmreclem4  16896  prmreclem5  16897  vdwlem1  16958  vdwlem2  16959  vdwlem9  16966  vdwlem10  16967  rami  16992  ramcl  17006  prmodvdslcmf  17024  prmgaplcmlem1  17028  cshwsidrepsw  17070  prdsbasprj  17441  isacs2  17620  acsfiel  17621  catidex  17641  iscatd2  17648  catlid  17650  catrid  17651  subcidcl  17812  funcid  17838  yonedalem4c  18244  yonffthlem  18249  isdrs2  18273  luble  18324  glble  18337  joinle  18351  meetle  18365  poslubmo  18376  posglbmo  18377  acsdrsel  18508  isacs4lem  18509  isacs5lem  18510  acsdrscl  18511  acsficl  18512  lidrideqd  18602  grpinvalem  18606  grpinva  18607  mndind  18761  grpidd2  18915  mulgsubcl  19026  issubg4  19083  ghmf1  19184  fislw  19561  efgsdmi  19668  efgsrel  19670  gexexlem  19788  gsumzaddlem  19857  gsummhm2  19875  dprdcntz  19946  dprddisj  19947  dprdss  19967  dprd2dlem2  19978  dprd2da  19980  dpjrid  20000  ablfac1eu  20011  pgpfac1lem1  20012  pgpfaclem2  20020  lringuplu  20459  issrngd  20770  islbs2  21070  lbsextlem4  21077  prmirredlem  21388  psgndiflemB  21515  frlmphl  21696  mplsubglem  21914  mpllsslem  21915  subrgasclcl  21980  mplind  21983  evlslem1  21995  ply1scleq  22198  mdetralt  22501  mdetunilem1  22505  lmcvg  23155  iscncl  23162  lmff  23194  cnrmi  23253  cmpcov  23282  fiuncmp  23297  hauscmplem  23299  1stcfb  23338  1stcelcls  23354  restnlly  23375  islly2  23377  lly1stc  23389  kgeni  23430  ptpjpre1  23464  ptbasfi  23474  ptpjopn  23505  dfac14  23511  txtube  23533  cnmpt11  23556  cnmpt21  23564  cnmptkp  23573  cnmptk1p  23578  qtopomap  23611  qtopcmap  23612  flimcf  23875  fclscf  23918  flfcntr  23936  ptcmplem3  23947  tgpt0  24012  tsmsi  24027  tsmsxplem2  24047  tsmsxp  24048  isucn2  24172  ucnima  24174  ucncn  24178  cfiluweak  24188  cuspcvg  24194  imasdsf1olem  24267  lpbl  24397  comet  24407  cfilucfil  24453  cnheiborlem  24859  cnheibor  24860  bndth  24863  nmoleub2lem2  25022  nmoleub3  25025  ipcau2  25141  tcphcphlem1  25142  tcphcphlem2  25143  lmmcvg  25168  cmetcaulem  25195  iscmet3lem1  25198  iscmet3lem2  25199  pjthlem1  25344  pjthlem2  25345  ivthlem1  25359  ivthlem2  25360  ivthlem3  25361  ivth2  25363  ivthle  25364  ivthle2  25365  ivthicc  25366  ovoliunlem1  25410  ovolshftlem1  25417  ovolscalem1  25421  ovolicc2lem3  25427  ovolicc2lem4  25428  ovolicc2  25430  volsup  25464  dyadmbl  25508  vitalilem2  25517  vitalilem3  25518  mbfdm  25534  ismbf3d  25562  cncombf  25566  itg2seq  25650  itg2monolem2  25659  itg2monolem3  25660  itg2mono  25661  iblitg  25676  itgconst  25727  itgfsum  25735  limcvallem  25779  cnlimci  25797  cnmptlimc  25798  dvferm1lem  25895  dvferm1  25896  dvferm2lem  25897  dvferm2  25898  dvlipcn  25906  dvle  25919  lhop1lem  25925  dvfsumge  25935  dvfsumlem2  25940  dvfsumlem2OLD  25941  dvfsumlem3  25942  ftc1a  25951  ftc1lem4  25953  itgsubstlem  25962  mdeglt  25977  deg1lt  26009  ply1divex  26049  fta1glem2  26081  fta1g  26082  plyco0  26104  plyeq0lem  26122  dgrcolem2  26187  plydivlem4  26211  plydivex  26212  fta1lem  26222  vieta1lem2  26226  vieta1  26227  tayl0  26276  ulmi  26302  ulmdvlem1  26316  ulmdvlem3  26318  ulmdv  26319  mtest  26320  pserulm  26338  efif1olem4  26461  rlimcnp  26882  rlimcnp2  26883  xrlimcnp  26885  scvxcvx  26903  lgamgulmlem5  26950  lgambdd  26954  lgamcvglem  26957  wilthlem2  26986  fsumdvdscom  27102  musumsum  27109  chtub  27130  fsumvma  27131  perfectlem2  27148  dchrelbas3  27156  dchrelbasd  27157  dchrn0  27168  dchrptlem2  27183  lgsval2lem  27225  lgsdirnn0  27262  lgsdinn0  27263  2sqlem10  27346  dchrisumlem1  27407  dchrmusum2  27412  dchrvmasumlem2  27416  dchrvmasumlem3  27417  dchrvmasumiflem1  27419  dchrisum0flblem2  27427  dchrisum0flb  27428  dchrisum0lem1b  27433  dchrisum0lem2  27436  2vmadivsumlem  27458  chpdifbndlem1  27471  selberg3lem1  27475  selberg4lem1  27478  pntrsumbnd2  27485  pntrlog2bndlem2  27496  pntrlog2bndlem3  27497  pntrlog2bndlem5  27499  pntrlog2bndlem6  27501  pntibndlem2  27509  pntibndlem3  27510  pntlemn  27518  pntlemj  27521  pntlemi  27522  pntlemo  27525  pntleme  27526  pntlem3  27527  pntlemp  27528  ostth2lem1  27536  ostthlem1  27545  ostth2lem2  27552  ostth3  27556  nosupprefixmo  27619  noinfprefixmo  27620  noinfbnd1lem1  27642  noinfbnd1lem4  27645  noinfbnd2lem1  27649  noinfbnd2  27650  cofsslt  27833  coinitsslt  27834  sleadd1  27903  addsass  27919  addsbdaylem  27930  negsid  27954  mulscom  28049  addsdilem3  28063  addsdilem4  28064  mulsasslem3  28075  precsexlem8  28123  precsexlem9  28124  precsexlem11  28126  n0sfincut  28253  onsfi  28254  zs12bday  28350  tglowdim1i  28435  tglowdim2ln  28585  wlkonl1iedg  29600  wlkp1lem7  29614  wlkp1lem8  29615  crctcshwlkn0lem6  29752  eupth2eucrct  30153  eupth2lem3  30172  ubthlem1  30806  ubthlem2  30807  minvecolem3  30812  occllem  31239  pjhthlem1  31327  eqelbid  32411  wrdt2ind  32883  mgccole1  32924  mgcmnt2  32927  dfmgc2  32930  chnltm1  32942  chnub  32946  fxpgaeq  33134  fxpsubm  33137  elrgspnlem4  33204  elrgspnsubrunlem2  33207  0nellinds  33349  linds2eq  33360  elrspunidl  33407  prmidl  33419  mxidlmax  33444  ssmxidl  33453  1arithidomlem1  33514  1arithidom  33516  1arithufdlem3  33525  1arithufdlem4  33526  ply1dg1rt  33556  lbsdiflsp0  33630  fedgmullem1  33633  fedgmullem2  33634  extdg1id  33669  fldextrspunlsplem  33676  constrsscn  33738  constrconj  33743  zrhcntr  33977  ofcfeqd2  34099  inelpisys  34152  unelldsys  34156  ldgenpisyslem1  34161  mbfmcnvima  34254  signstfvneq0  34571  fsum2dsub  34606  hgt750lemc  34646  hgt750lemd  34647  hgt749d  34648  hgt750lemf  34652  bnj1379  34828  bnj1450  35048  revwlk  35114  subfacp1lem5  35173  cvmlift2lem10  35301  weiunfrlem  36449  weiunpo  36450  weiunso  36451  weiunfr  36452  weiunse  36453  unblimceq0lem  36491  unblimceq0  36492  unbdqndv2  36496  bj-ismoored  37092  lcmineqlem4  42012  dvle2  42052  aks4d1p9  42068  primrootlekpowne0  42085  aks6d1c1p3  42090  aks6d1c1p4  42091  aks6d1c1p5  42092  aks6d1c1  42096  hashscontpow  42102  aks6d1c2lem3  42106  sticksstones1  42126  aks6d1c6lem1  42150  aks6d1c6lem2  42151  aks6d1c6lem4  42153  aks6d1c7  42164  aks5lem3a  42169  unitscyglem1  42175  unitscyglem2  42176  unitscyglem3  42177  unitscyglem4  42178  exfinfldd  42183  fnwe2lem2  43012  aomclem4  43018  scottelrankd  44208  mnuop123d  44223  mnuprdlem1  44233  mnuprdlem2  44234  eliind  45037  rnmptbd2lem  45214  rnmptbdlem  45221  cvgcau  45459  limclner  45622  climisp  45717  climrescn  45719  climxrrelem  45720  climxrre  45721  liminflelimsuplem  45746  cncfshift  45845  cncfperiod  45850  fperdvper  45890  salunicl  46287  saldifcl  46290  meadjuni  46428  lubsscl  48876  glbsscl  48877  ipolub  48904  ipoglb  48907  ssccatid  48989  upciclem1  49074  oppcup3lem  49113  oppcthinendcALT  49319  setcthin  49343