Theorem rspcdva 3586

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045

This theorem is referenced by:  nvocnv  7238  knatar  7314  caofref  7664  caofinvl  7665  tfisi  7815  frxp2  8100  frxp3  8107  suppssov1  8153  suppssov2  8154  fpr3g  8241  fprresex  8266  tfrlem1  8321  tfrlem5  8325  coflton  8612  cofon1  8613  cofon2  8614  marypha1lem  9360  marypha1  9361  ordtypelem6  9452  ordtypelem7  9453  wemaplem2  9476  oemapvali  9613  cantnflem1c  9616  ttrcltr  9645  ttrclss  9649  dmttrcl  9650  rnttrcl  9651  ttrclselem2  9655  infxpenlem  9942  acni  9974  dfac9  10066  dfac12lem2  10074  sornom  10206  fin1ai  10222  fin2i  10224  fin23lem11  10246  isfin2-2  10248  fin23lem17  10267  fin23lem39  10279  fin1a2lem13  10341  hsmexlem4  10358  ttukeylem5  10442  ttukeylem6  10443  canth4  10576  pwfseqlem5  10592  winalim2  10625  wununi  10635  wunpw  10636  dedekind  11313  zsupss  12872  uzwo3  12878  seqcl2  13961  seqcl  13963  seqf  13964  seqfveq2  13965  seqfveq  13967  seqshft2  13969  monoord  13973  monoord2  13974  sermono  13975  seqsplit  13976  seqcaopr3  13978  seqid  13988  seqid2  13989  seqhomo  13990  seqz  13991  discr1  14180  discr  14181  hashbclem  14393  wrdind  14663  limsupgre  15423  climi  15452  rlimi  15455  rlimclim1  15487  rlimclim  15488  climrlim2  15489  rlimcn1  15530  climcn1  15534  isercoll2  15611  caucvgrlem  15615  caucvgb  15622  iseraltlem2  15625  iseraltlem3  15626  fsumm1  15693  fsum1p  15695  fsumcom2  15716  fsumge1  15739  telfsumo  15744  telfsumo2  15745  fsumparts  15748  o1fsum  15755  isum1p  15783  isumnn0nn  15784  isumrpcl  15785  climcndslem1  15791  climcndslem2  15792  climcnds  15793  cvgrat  15825  mertenslem1  15826  mertens  15828  fprodm1  15909  fprod1p  15910  fprodcom2  15926  prmind2  16631  pcmpt2  16840  prmpwdvds  16851  prmreclem4  16866  prmreclem5  16867  vdwlem1  16928  vdwlem2  16929  vdwlem9  16936  vdwlem10  16937  rami  16962  ramcl  16976  prmodvdslcmf  16994  prmgaplcmlem1  16998  cshwsidrepsw  17040  prdsbasprj  17411  isacs2  17590  acsfiel  17591  catidex  17611  iscatd2  17618  catlid  17620  catrid  17621  subcidcl  17782  funcid  17808  yonedalem4c  18214  yonffthlem  18219  isdrs2  18243  luble  18294  glble  18307  joinle  18321  meetle  18335  poslubmo  18346  posglbmo  18347  acsdrsel  18478  isacs4lem  18479  isacs5lem  18480  acsdrscl  18481  acsficl  18482  lidrideqd  18572  grpinvalem  18576  grpinva  18577  mndind  18731  grpidd2  18885  mulgsubcl  18996  issubg4  19053  ghmf1  19154  fislw  19531  efgsdmi  19638  efgsrel  19640  gexexlem  19758  gsumzaddlem  19827  gsummhm2  19845  dprdcntz  19916  dprddisj  19917  dprdss  19937  dprd2dlem2  19948  dprd2da  19950  dpjrid  19970  ablfac1eu  19981  pgpfac1lem1  19982  pgpfaclem2  19990  lringuplu  20429  issrngd  20740  islbs2  21040  lbsextlem4  21047  prmirredlem  21358  psgndiflemB  21485  frlmphl  21666  mplsubglem  21884  mpllsslem  21885  subrgasclcl  21950  mplind  21953  evlslem1  21965  ply1scleq  22168  mdetralt  22471  mdetunilem1  22475  lmcvg  23125  iscncl  23132  lmff  23164  cnrmi  23223  cmpcov  23252  fiuncmp  23267  hauscmplem  23269  1stcfb  23308  1stcelcls  23324  restnlly  23345  islly2  23347  lly1stc  23359  kgeni  23400  ptpjpre1  23434  ptbasfi  23444  ptpjopn  23475  dfac14  23481  txtube  23503  cnmpt11  23526  cnmpt21  23534  cnmptkp  23543  cnmptk1p  23548  qtopomap  23581  qtopcmap  23582  flimcf  23845  fclscf  23888  flfcntr  23906  ptcmplem3  23917  tgpt0  23982  tsmsi  23997  tsmsxplem2  24017  tsmsxp  24018  isucn2  24142  ucnima  24144  ucncn  24148  cfiluweak  24158  cuspcvg  24164  imasdsf1olem  24237  lpbl  24367  comet  24377  cfilucfil  24423  cnheiborlem  24829  cnheibor  24830  bndth  24833  nmoleub2lem2  24992  nmoleub3  24995  ipcau2  25110  tcphcphlem1  25111  tcphcphlem2  25112  lmmcvg  25137  cmetcaulem  25164  iscmet3lem1  25167  iscmet3lem2  25168  pjthlem1  25313  pjthlem2  25314  ivthlem1  25328  ivthlem2  25329  ivthlem3  25330  ivth2  25332  ivthle  25333  ivthle2  25334  ivthicc  25335  ovoliunlem1  25379  ovolshftlem1  25386  ovolscalem1  25390  ovolicc2lem3  25396  ovolicc2lem4  25397  ovolicc2  25399  volsup  25433  dyadmbl  25477  vitalilem2  25486  vitalilem3  25487  mbfdm  25503  ismbf3d  25531  cncombf  25535  itg2seq  25619  itg2monolem2  25628  itg2monolem3  25629  itg2mono  25630  iblitg  25645  itgconst  25696  itgfsum  25704  limcvallem  25748  cnlimci  25766  cnmptlimc  25767  dvferm1lem  25864  dvferm1  25865  dvferm2lem  25866  dvferm2  25867  dvlipcn  25875  dvle  25888  lhop1lem  25894  dvfsumge  25904  dvfsumlem2  25909  dvfsumlem2OLD  25910  dvfsumlem3  25911  ftc1a  25920  ftc1lem4  25922  itgsubstlem  25931  mdeglt  25946  deg1lt  25978  ply1divex  26018  fta1glem2  26050  fta1g  26051  plyco0  26073  plyeq0lem  26091  dgrcolem2  26156  plydivlem4  26180  plydivex  26181  fta1lem  26191  vieta1lem2  26195  vieta1  26196  tayl0  26245  ulmi  26271  ulmdvlem1  26285  ulmdvlem3  26287  ulmdv  26288  mtest  26289  pserulm  26307  efif1olem4  26430  rlimcnp  26851  rlimcnp2  26852  xrlimcnp  26854  scvxcvx  26872  lgamgulmlem5  26919  lgambdd  26923  lgamcvglem  26926  wilthlem2  26955  fsumdvdscom  27071  musumsum  27078  chtub  27099  fsumvma  27100  perfectlem2  27117  dchrelbas3  27125  dchrelbasd  27126  dchrn0  27137  dchrptlem2  27152  lgsval2lem  27194  lgsdirnn0  27231  lgsdinn0  27232  2sqlem10  27315  dchrisumlem1  27376  dchrmusum2  27381  dchrvmasumlem2  27385  dchrvmasumlem3  27386  dchrvmasumiflem1  27388  dchrisum0flblem2  27396  dchrisum0flb  27397  dchrisum0lem1b  27402  dchrisum0lem2  27405  2vmadivsumlem  27427  chpdifbndlem1  27440  selberg3lem1  27444  selberg4lem1  27447  pntrsumbnd2  27454  pntrlog2bndlem2  27465  pntrlog2bndlem3  27466  pntrlog2bndlem5  27468  pntrlog2bndlem6  27470  pntibndlem2  27478  pntibndlem3  27479  pntlemn  27487  pntlemj  27490  pntlemi  27491  pntlemo  27494  pntleme  27495  pntlem3  27496  pntlemp  27497  ostth2lem1  27505  ostthlem1  27514  ostth2lem2  27521  ostth3  27525  nosupprefixmo  27588  noinfprefixmo  27589  noinfbnd1lem1  27611  noinfbnd1lem4  27614  noinfbnd2lem1  27618  noinfbnd2  27619  cofsslt  27802  coinitsslt  27803  sleadd1  27872  addsass  27888  addsbdaylem  27899  negsid  27923  mulscom  28018  addsdilem3  28032  addsdilem4  28033  mulsasslem3  28044  precsexlem8  28092  precsexlem9  28093  precsexlem11  28095  n0sfincut  28222  onsfi  28223  zs12bday  28319  tglowdim1i  28404  tglowdim2ln  28554  wlkonl1iedg  29567  wlkp1lem7  29581  wlkp1lem8  29582  crctcshwlkn0lem6  29718  eupth2eucrct  30119  eupth2lem3  30138  ubthlem1  30772  ubthlem2  30773  minvecolem3  30778  occllem  31205  pjhthlem1  31293  eqelbid  32377  wrdt2ind  32848  mgccole1  32889  mgcmnt2  32892  dfmgc2  32895  chnltm1  32907  chnub  32911  fxpgaeq  33099  fxpsubm  33102  elrgspnlem4  33169  elrgspnsubrunlem2  33172  0nellinds  33314  linds2eq  33325  elrspunidl  33372  prmidl  33384  mxidlmax  33409  ssmxidl  33418  1arithidomlem1  33479  1arithidom  33481  1arithufdlem3  33490  1arithufdlem4  33491  ply1dg1rt  33521  lbsdiflsp0  33595  fedgmullem1  33598  fedgmullem2  33599  extdg1id  33634  fldextrspunlsplem  33641  constrsscn  33703  constrconj  33708  zrhcntr  33942  ofcfeqd2  34064  inelpisys  34117  unelldsys  34121  ldgenpisyslem1  34126  mbfmcnvima  34219  signstfvneq0  34536  fsum2dsub  34571  hgt750lemc  34611  hgt750lemd  34612  hgt749d  34613  hgt750lemf  34617  bnj1379  34793  bnj1450  35013  revwlk  35085  subfacp1lem5  35144  cvmlift2lem10  35272  weiunfrlem  36425  weiunpo  36426  weiunso  36427  weiunfr  36428  weiunse  36429  unblimceq0lem  36467  unblimceq0  36468  unbdqndv2  36472  bj-ismoored  37068  lcmineqlem4  41993  dvle2  42033  aks4d1p9  42049  primrootlekpowne0  42066  aks6d1c1p3  42071  aks6d1c1p4  42072  aks6d1c1p5  42073  aks6d1c1  42077  hashscontpow  42083  aks6d1c2lem3  42087  sticksstones1  42107  aks6d1c6lem1  42131  aks6d1c6lem2  42132  aks6d1c6lem4  42134  aks6d1c7  42145  aks5lem3a  42150  unitscyglem1  42156  unitscyglem2  42157  unitscyglem3  42158  unitscyglem4  42159  exfinfldd  42164  fnwe2lem2  43013  aomclem4  43019  scottelrankd  44209  mnuop123d  44224  mnuprdlem1  44234  mnuprdlem2  44235  eliind  45038  rnmptbd2lem  45215  rnmptbdlem  45222  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  48921  glbsscl  48922  ipolub  48949  ipoglb  48952  ssccatid  49034  upciclem1  49128  oppcup3lem  49168  oppcthinendcALT  49403  setcthin  49427