Theorem rspcdva 3574

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  ∀wral 3048

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049

This theorem is referenced by:  nvocnv  7224  knatar  7300  caofref  7650  caofinvl  7651  tfisi  7798  frxp2  8083  frxp3  8090  suppssov1  8136  suppssov2  8137  fpr3g  8224  fprresex  8249  tfrlem1  8304  tfrlem5  8308  coflton  8595  cofon1  8596  cofon2  8597  marypha1lem  9328  marypha1  9329  ordtypelem6  9420  ordtypelem7  9421  wemaplem2  9444  oemapvali  9585  cantnflem1c  9588  ttrcltr  9617  ttrclss  9621  dmttrcl  9622  rnttrcl  9623  ttrclselem2  9627  infxpenlem  9915  acni  9947  dfac9  10039  dfac12lem2  10047  sornom  10179  fin1ai  10195  fin2i  10197  fin23lem11  10219  isfin2-2  10221  fin23lem17  10240  fin23lem39  10252  fin1a2lem13  10314  hsmexlem4  10331  ttukeylem5  10415  ttukeylem6  10416  canth4  10549  pwfseqlem5  10565  winalim2  10598  wununi  10608  wunpw  10609  dedekind  11287  zsupss  12841  uzwo3  12847  seqcl2  13934  seqcl  13936  seqf  13937  seqfveq2  13938  seqfveq  13940  seqshft2  13942  monoord  13946  monoord2  13947  sermono  13948  seqsplit  13949  seqcaopr3  13951  seqid  13961  seqid2  13962  seqhomo  13963  seqz  13964  discr1  14153  discr  14154  hashbclem  14366  wrdind  14636  limsupgre  15395  climi  15424  rlimi  15427  rlimclim1  15459  rlimclim  15460  climrlim2  15461  rlimcn1  15502  climcn1  15506  isercoll2  15583  caucvgrlem  15587  caucvgb  15594  iseraltlem2  15597  iseraltlem3  15598  fsumm1  15665  fsum1p  15667  fsumcom2  15688  fsumge1  15711  telfsumo  15716  telfsumo2  15717  fsumparts  15720  o1fsum  15727  isum1p  15755  isumnn0nn  15756  isumrpcl  15757  climcndslem1  15763  climcndslem2  15764  climcnds  15765  cvgrat  15797  mertenslem1  15798  mertens  15800  fprodm1  15881  fprod1p  15882  fprodcom2  15898  prmind2  16603  pcmpt2  16812  prmpwdvds  16823  prmreclem4  16838  prmreclem5  16839  vdwlem1  16900  vdwlem2  16901  vdwlem9  16908  vdwlem10  16909  rami  16934  ramcl  16948  prmodvdslcmf  16966  prmgaplcmlem1  16970  cshwsidrepsw  17012  prdsbasprj  17383  isacs2  17567  acsfiel  17568  catidex  17588  iscatd2  17595  catlid  17597  catrid  17598  subcidcl  17759  funcid  17785  yonedalem4c  18191  yonffthlem  18196  isdrs2  18220  luble  18271  glble  18284  joinle  18298  meetle  18312  poslubmo  18323  posglbmo  18324  acsdrsel  18457  isacs4lem  18458  isacs5lem  18459  acsdrscl  18460  acsficl  18461  chnltm1  18523  chnub  18536  lidrideqd  18585  grpinvalem  18589  grpinva  18590  mndind  18744  grpidd2  18898  mulgsubcl  19009  issubg4  19066  ghmf1  19166  fislw  19545  efgsdmi  19652  efgsrel  19654  gexexlem  19772  gsumzaddlem  19841  gsummhm2  19859  dprdcntz  19930  dprddisj  19931  dprdss  19951  dprd2dlem2  19962  dprd2da  19964  dpjrid  19984  ablfac1eu  19995  pgpfac1lem1  19996  pgpfaclem2  20004  lringuplu  20468  issrngd  20779  islbs2  21100  lbsextlem4  21107  prmirredlem  21418  psgndiflemB  21546  frlmphl  21727  mplsubglem  21945  mpllsslem  21946  subrgasclcl  22013  mplind  22016  evlslem1  22028  ply1scleq  22240  mdetralt  22543  mdetunilem1  22547  lmcvg  23197  iscncl  23204  lmff  23236  cnrmi  23295  cmpcov  23324  fiuncmp  23339  hauscmplem  23341  1stcfb  23380  1stcelcls  23396  restnlly  23417  islly2  23419  lly1stc  23431  kgeni  23472  ptpjpre1  23506  ptbasfi  23516  ptpjopn  23547  dfac14  23553  txtube  23575  cnmpt11  23598  cnmpt21  23606  cnmptkp  23615  cnmptk1p  23620  qtopomap  23653  qtopcmap  23654  flimcf  23917  fclscf  23960  flfcntr  23978  ptcmplem3  23989  tgpt0  24054  tsmsi  24069  tsmsxplem2  24089  tsmsxp  24090  isucn2  24213  ucnima  24215  ucncn  24219  cfiluweak  24229  cuspcvg  24235  imasdsf1olem  24308  lpbl  24438  comet  24448  cfilucfil  24494  cnheiborlem  24900  cnheibor  24901  bndth  24904  nmoleub2lem2  25063  nmoleub3  25066  ipcau2  25181  tcphcphlem1  25182  tcphcphlem2  25183  lmmcvg  25208  cmetcaulem  25235  iscmet3lem1  25238  iscmet3lem2  25239  pjthlem1  25384  pjthlem2  25385  ivthlem1  25399  ivthlem2  25400  ivthlem3  25401  ivth2  25403  ivthle  25404  ivthle2  25405  ivthicc  25406  ovoliunlem1  25450  ovolshftlem1  25457  ovolscalem1  25461  ovolicc2lem3  25467  ovolicc2lem4  25468  ovolicc2  25470  volsup  25504  dyadmbl  25548  vitalilem2  25557  vitalilem3  25558  mbfdm  25574  ismbf3d  25602  cncombf  25606  itg2seq  25690  itg2monolem2  25699  itg2monolem3  25700  itg2mono  25701  iblitg  25716  itgconst  25767  itgfsum  25775  limcvallem  25819  cnlimci  25837  cnmptlimc  25838  dvferm1lem  25935  dvferm1  25936  dvferm2lem  25937  dvferm2  25938  dvlipcn  25946  dvle  25959  lhop1lem  25965  dvfsumge  25975  dvfsumlem2  25980  dvfsumlem2OLD  25981  dvfsumlem3  25982  ftc1a  25991  ftc1lem4  25993  itgsubstlem  26002  mdeglt  26017  deg1lt  26049  ply1divex  26089  fta1glem2  26121  fta1g  26122  plyco0  26144  plyeq0lem  26162  dgrcolem2  26227  plydivlem4  26251  plydivex  26252  fta1lem  26262  vieta1lem2  26266  vieta1  26267  tayl0  26316  ulmi  26342  ulmdvlem1  26356  ulmdvlem3  26358  ulmdv  26359  mtest  26360  pserulm  26378  efif1olem4  26501  rlimcnp  26922  rlimcnp2  26923  xrlimcnp  26925  scvxcvx  26943  lgamgulmlem5  26990  lgambdd  26994  lgamcvglem  26997  wilthlem2  27026  fsumdvdscom  27142  musumsum  27149  chtub  27170  fsumvma  27171  perfectlem2  27188  dchrelbas3  27196  dchrelbasd  27197  dchrn0  27208  dchrptlem2  27223  lgsval2lem  27265  lgsdirnn0  27302  lgsdinn0  27303  2sqlem10  27386  dchrisumlem1  27447  dchrmusum2  27452  dchrvmasumlem2  27456  dchrvmasumlem3  27457  dchrvmasumiflem1  27459  dchrisum0flblem2  27467  dchrisum0flb  27468  dchrisum0lem1b  27473  dchrisum0lem2  27476  2vmadivsumlem  27498  chpdifbndlem1  27511  selberg3lem1  27515  selberg4lem1  27518  pntrsumbnd2  27525  pntrlog2bndlem2  27536  pntrlog2bndlem3  27537  pntrlog2bndlem5  27539  pntrlog2bndlem6  27541  pntibndlem2  27549  pntibndlem3  27550  pntlemn  27558  pntlemj  27561  pntlemi  27562  pntlemo  27565  pntleme  27566  pntlem3  27567  pntlemp  27568  ostth2lem1  27576  ostthlem1  27585  ostth2lem2  27592  ostth3  27596  nosupprefixmo  27659  noinfprefixmo  27660  noinfbnd1lem1  27682  noinfbnd1lem4  27685  noinfbnd2lem1  27689  noinfbnd2  27690  eqscut3  27785  cofsslt  27882  coinitsslt  27883  sleadd1  27952  addsass  27968  addsbdaylem  27979  negsid  28003  mulscom  28098  addsdilem3  28112  addsdilem4  28113  mulsasslem3  28124  precsexlem8  28172  precsexlem9  28173  precsexlem11  28175  n0sfincut  28302  onsfi  28303  zs12bday  28414  tglowdim1i  28499  tglowdim2ln  28649  wlkonl1iedg  29663  wlkp1lem7  29677  wlkp1lem8  29678  crctcshwlkn0lem6  29814  eupth2eucrct  30218  eupth2lem3  30237  ubthlem1  30871  ubthlem2  30872  minvecolem3  30877  occllem  31304  pjhthlem1  31392  eqelbid  32475  fnfvor  32613  ofrco  32614  wrdt2ind  32963  mgccole1  33000  mgcmnt2  33003  dfmgc2  33006  fxpgaeq  33179  fxpsubm  33182  fxpsubg  33183  fxpsubrg  33184  elrgspnlem4  33255  elrgspnsubrunlem2  33258  0nellinds  33379  linds2eq  33390  elrspunidl  33437  prmidl  33449  mxidlmax  33474  ssmxidl  33483  1arithidomlem1  33544  1arithidom  33546  1arithufdlem3  33555  1arithufdlem4  33556  ply1dg1rt  33589  vietalem  33663  lbsdiflsp0  33711  fedgmullem1  33714  fedgmullem2  33715  extdg1id  33751  fldextrspunlsplem  33758  extdgfialglem2  33778  constrsscn  33825  constrconj  33830  zrhcntr  34064  ofcfeqd2  34186  inelpisys  34239  unelldsys  34243  ldgenpisyslem1  34248  mbfmcnvima  34340  signstfvneq0  34657  fsum2dsub  34692  hgt750lemc  34732  hgt750lemd  34733  hgt749d  34734  hgt750lemf  34738  bnj1379  34914  bnj1450  35134  revwlk  35241  subfacp1lem5  35300  cvmlift2lem10  35428  weiunfrlem  36580  weiunpo  36581  weiunso  36582  weiunfr  36583  weiunse  36584  unblimceq0lem  36622  unblimceq0  36623  unbdqndv2  36627  bj-ismoored  37224  lcmineqlem4  42198  dvle2  42238  aks4d1p9  42254  primrootlekpowne0  42271  aks6d1c1p3  42276  aks6d1c1p4  42277  aks6d1c1p5  42278  aks6d1c1  42282  hashscontpow  42288  aks6d1c2lem3  42292  sticksstones1  42312  aks6d1c6lem1  42336  aks6d1c6lem2  42337  aks6d1c6lem4  42339  aks6d1c7  42350  aks5lem3a  42355  unitscyglem1  42361  unitscyglem2  42362  unitscyglem3  42363  unitscyglem4  42364  exfinfldd  42369  fnwe2lem2  43208  aomclem4  43214  scottelrankd  44404  mnuop123d  44419  mnuprdlem1  44429  mnuprdlem2  44430  eliind  45232  rnmptbd2lem  45408  rnmptbdlem  45415  cvgcau  45650  limclner  45811  climisp  45906  climrescn  45908  climxrrelem  45909  climxrre  45910  liminflelimsuplem  45935  cncfshift  46034  cncfperiod  46039  fperdvper  46079  salunicl  46476  saldifcl  46479  meadjuni  46617  chnerlem1  47042  lubsscl  49121  glbsscl  49122  ipolub  49149  ipoglb  49152  ssccatid  49233  upciclem1  49327  oppcup3lem  49367  oppcthinendcALT  49602  setcthin  49626