Theorem rspcdva 3623

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2106  ∀wral 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060

This theorem is referenced by:  nvocnv  7301  knatar  7377  caofref  7728  caofinvl  7729  tfisi  7880  frxp2  8168  frxp3  8175  suppssov1  8221  suppssov2  8222  fpr3g  8309  fprresex  8334  wfrlem17OLD  8364  tfrlem1  8415  tfrlem5  8419  coflton  8708  cofon1  8709  cofon2  8710  marypha1lem  9471  marypha1  9472  ordtypelem6  9561  ordtypelem7  9562  wemaplem2  9585  oemapvali  9722  cantnflem1c  9725  ttrcltr  9754  ttrclss  9758  dmttrcl  9759  rnttrcl  9760  ttrclselem2  9764  infxpenlem  10051  acni  10083  dfac9  10175  dfac12lem2  10183  sornom  10315  fin1ai  10331  fin2i  10333  fin23lem11  10355  isfin2-2  10357  fin23lem17  10376  fin23lem39  10388  fin1a2lem13  10450  hsmexlem4  10467  ttukeylem5  10551  ttukeylem6  10552  canth4  10685  pwfseqlem5  10701  winalim2  10734  wununi  10744  wunpw  10745  dedekind  11422  zsupss  12977  uzwo3  12983  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  14275  discr  14276  hashbclem  14488  wrdind  14757  limsupgre  15514  climi  15543  rlimi  15546  rlimclim1  15578  rlimclim  15579  climrlim2  15580  rlimcn1  15621  climcn1  15625  isercoll2  15702  caucvgrlem  15706  caucvgb  15713  iseraltlem2  15716  iseraltlem3  15717  fsumm1  15784  fsum1p  15786  fsumcom2  15807  fsumge1  15830  telfsumo  15835  telfsumo2  15836  fsumparts  15839  o1fsum  15846  isum1p  15874  isumnn0nn  15875  isumrpcl  15876  climcndslem1  15882  climcndslem2  15883  climcnds  15884  cvgrat  15916  mertenslem1  15917  mertens  15919  fprodm1  16000  fprod1p  16001  fprodcom2  16017  prmind2  16719  pcmpt2  16927  prmpwdvds  16938  prmreclem4  16953  prmreclem5  16954  vdwlem1  17015  vdwlem2  17016  vdwlem9  17023  vdwlem10  17024  rami  17049  ramcl  17063  prmodvdslcmf  17081  prmgaplcmlem1  17085  cshwsidrepsw  17128  prdsbasprj  17519  isacs2  17698  acsfiel  17699  catidex  17719  iscatd2  17726  catlid  17728  catrid  17729  subcidcl  17895  funcid  17921  yonedalem4c  18334  yonffthlem  18339  isdrs2  18364  luble  18417  glble  18430  joinle  18444  meetle  18458  poslubmo  18469  posglbmo  18470  acsdrsel  18601  isacs4lem  18602  isacs5lem  18603  acsdrscl  18604  acsficl  18605  lidrideqd  18695  grpinvalem  18699  grpinva  18700  mndind  18854  grpidd2  19008  mulgsubcl  19119  issubg4  19176  ghmf1  19277  fislw  19658  efgsdmi  19765  efgsrel  19767  gexexlem  19885  gsumzaddlem  19954  gsummhm2  19972  dprdcntz  20043  dprddisj  20044  dprdss  20064  dprd2dlem2  20075  dprd2da  20077  dpjrid  20097  ablfac1eu  20108  pgpfac1lem1  20109  pgpfaclem2  20117  lringuplu  20561  issrngd  20873  islbs2  21174  lbsextlem4  21181  prmirredlem  21501  psgndiflemB  21636  frlmphl  21819  mplsubglem  22037  mpllsslem  22038  subrgasclcl  22109  mplind  22112  evlslem1  22124  ply1scleq  22325  mdetralt  22630  mdetunilem1  22634  lmcvg  23286  iscncl  23293  lmff  23325  cnrmi  23384  cmpcov  23413  fiuncmp  23428  hauscmplem  23430  1stcfb  23469  1stcelcls  23485  restnlly  23506  islly2  23508  lly1stc  23520  kgeni  23561  ptpjpre1  23595  ptbasfi  23605  ptpjopn  23636  dfac14  23642  txtube  23664  cnmpt11  23687  cnmpt21  23695  cnmptkp  23704  cnmptk1p  23709  qtopomap  23742  qtopcmap  23743  flimcf  24006  fclscf  24049  flfcntr  24067  ptcmplem3  24078  tgpt0  24143  tsmsi  24158  tsmsxplem2  24178  tsmsxp  24179  isucn2  24304  ucnima  24306  ucncn  24310  cfiluweak  24320  cuspcvg  24326  imasdsf1olem  24399  lpbl  24532  comet  24542  cfilucfil  24588  cnheiborlem  25000  cnheibor  25001  bndth  25004  nmoleub2lem2  25163  nmoleub3  25166  ipcau2  25282  tcphcphlem1  25283  tcphcphlem2  25284  lmmcvg  25309  cmetcaulem  25336  iscmet3lem1  25339  iscmet3lem2  25340  pjthlem1  25485  pjthlem2  25486  ivthlem1  25500  ivthlem2  25501  ivthlem3  25502  ivth2  25504  ivthle  25505  ivthle2  25506  ivthicc  25507  ovoliunlem1  25551  ovolshftlem1  25558  ovolscalem1  25562  ovolicc2lem3  25568  ovolicc2lem4  25569  ovolicc2  25571  volsup  25605  dyadmbl  25649  vitalilem2  25658  vitalilem3  25659  mbfdm  25675  ismbf3d  25703  cncombf  25707  itg2seq  25792  itg2monolem2  25801  itg2monolem3  25802  itg2mono  25803  iblitg  25818  itgconst  25869  itgfsum  25877  limcvallem  25921  cnlimci  25939  cnmptlimc  25940  dvferm1lem  26037  dvferm1  26038  dvferm2lem  26039  dvferm2  26040  dvlipcn  26048  dvle  26061  lhop1lem  26067  dvfsumge  26077  dvfsumlem2  26082  dvfsumlem2OLD  26083  dvfsumlem3  26084  ftc1a  26093  ftc1lem4  26095  itgsubstlem  26104  mdeglt  26119  deg1lt  26151  ply1divex  26191  fta1glem2  26223  fta1g  26224  plyco0  26246  plyeq0lem  26264  dgrcolem2  26329  plydivlem4  26353  plydivex  26354  fta1lem  26364  vieta1lem2  26368  vieta1  26369  tayl0  26418  ulmi  26444  ulmdvlem1  26458  ulmdvlem3  26460  ulmdv  26461  mtest  26462  pserulm  26480  efif1olem4  26602  rlimcnp  27023  rlimcnp2  27024  xrlimcnp  27026  scvxcvx  27044  lgamgulmlem5  27091  lgambdd  27095  lgamcvglem  27098  wilthlem2  27127  fsumdvdscom  27243  musumsum  27250  chtub  27271  fsumvma  27272  perfectlem2  27289  dchrelbas3  27297  dchrelbasd  27298  dchrn0  27309  dchrptlem2  27324  lgsval2lem  27366  lgsdirnn0  27403  lgsdinn0  27404  2sqlem10  27487  dchrisumlem1  27548  dchrmusum2  27553  dchrvmasumlem2  27557  dchrvmasumlem3  27558  dchrvmasumiflem1  27560  dchrisum0flblem2  27568  dchrisum0flb  27569  dchrisum0lem1b  27574  dchrisum0lem2  27577  2vmadivsumlem  27599  chpdifbndlem1  27612  selberg3lem1  27616  selberg4lem1  27619  pntrsumbnd2  27626  pntrlog2bndlem2  27637  pntrlog2bndlem3  27638  pntrlog2bndlem5  27640  pntrlog2bndlem6  27642  pntibndlem2  27650  pntibndlem3  27651  pntlemn  27659  pntlemj  27662  pntlemi  27663  pntlemo  27666  pntleme  27667  pntlem3  27668  pntlemp  27669  ostth2lem1  27677  ostthlem1  27686  ostth2lem2  27693  ostth3  27697  nosupprefixmo  27760  noinfprefixmo  27761  noinfbnd1lem1  27783  noinfbnd1lem4  27786  noinfbnd2lem1  27790  noinfbnd2  27791  cofsslt  27967  coinitsslt  27968  sleadd1  28037  addsass  28053  addsbdaylem  28064  negsid  28088  mulscom  28180  addsdilem3  28194  addsdilem4  28195  mulsasslem3  28206  precsexlem8  28253  precsexlem9  28254  precsexlem11  28256  zs12bday  28439  tglowdim1i  28524  tglowdim2ln  28674  wlkonl1iedg  29698  wlkp1lem7  29712  wlkp1lem8  29713  crctcshwlkn0lem6  29845  eupth2eucrct  30246  eupth2lem3  30265  ubthlem1  30899  ubthlem2  30900  minvecolem3  30905  occllem  31332  pjhthlem1  31420  eqelbid  32503  wrdt2ind  32923  mgccole1  32965  mgcmnt2  32968  dfmgc2  32971  chnltm1  32983  chnub  32986  elrgspnlem4  33235  0nellinds  33378  linds2eq  33389  elrspunidl  33436  prmidl  33448  mxidlmax  33473  ssmxidl  33482  1arithidomlem1  33543  1arithidom  33545  1arithufdlem3  33554  1arithufdlem4  33555  ply1dg1rt  33584  lbsdiflsp0  33654  fedgmullem1  33657  fedgmullem2  33658  extdg1id  33691  constrsscn  33745  constrconj  33750  zrhcntr  33942  ofcfeqd2  34082  inelpisys  34135  unelldsys  34139  ldgenpisyslem1  34144  mbfmcnvima  34237  signstfvneq0  34566  fsum2dsub  34601  hgt750lemc  34641  hgt750lemd  34642  hgt749d  34643  hgt750lemf  34647  bnj1379  34823  bnj1450  35043  revwlk  35109  subfacp1lem5  35169  cvmlift2lem10  35297  weiunfrlem  36447  weiunpo  36448  weiunso  36449  weiunfr  36450  weiunse  36451  unblimceq0lem  36489  unblimceq0  36490  unbdqndv2  36494  bj-ismoored  37090  lcmineqlem4  42014  dvle2  42054  aks4d1p9  42070  primrootlekpowne0  42087  aks6d1c1p3  42092  aks6d1c1p4  42093  aks6d1c1p5  42094  aks6d1c1  42098  hashscontpow  42104  aks6d1c2lem3  42108  sticksstones1  42128  aks6d1c6lem1  42152  aks6d1c6lem2  42153  aks6d1c6lem4  42155  aks6d1c7  42166  aks5lem3a  42171  unitscyglem1  42177  unitscyglem2  42178  unitscyglem3  42179  unitscyglem4  42180  exfinfldd  42185  fnwe2lem2  43040  aomclem4  43046  scottelrankd  44243  mnuop123d  44258  mnuprdlem1  44268  mnuprdlem2  44269  eliind  45011  rnmptbd2lem  45193  rnmptbdlem  45200  cvgcau  45441  limclner  45607  climisp  45702  climrescn  45704  climxrrelem  45705  climxrre  45706  cncfshift  45830  cncfperiod  45835  fperdvper  45875  salunicl  46272  saldifcl  46275  meadjuni  46413  lubsscl  48757  glbsscl  48758  ipolub  48777  ipoglb  48780  upciclem1  48812  setcthin  48856