Theorem rspcdva 3562

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2109  ∀wral 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070

This theorem is referenced by:  nvocnv  7147  knatar  7221  caofref  7553  caofinvl  7554  tfisi  7693  suppssov1  7998  fpr3g  8085  fprresex  8110  wfrlem17OLD  8140  tfrlem1  8191  tfrlem5  8195  marypha1lem  9153  marypha1  9154  ordtypelem6  9243  ordtypelem7  9244  wemaplem2  9267  oemapvali  9403  cantnflem1c  9406  ttrcltr  9435  ttrclss  9439  dmttrcl  9440  rnttrcl  9441  ttrclselem2  9445  infxpenlem  9753  acni  9785  dfac9  9876  dfac12lem2  9884  sornom  10017  fin1ai  10033  fin2i  10035  fin23lem11  10057  isfin2-2  10059  fin23lem17  10078  fin23lem39  10090  fin1a2lem13  10152  hsmexlem4  10169  ttukeylem5  10253  ttukeylem6  10254  canth4  10387  pwfseqlem5  10403  winalim2  10436  wununi  10446  wunpw  10447  dedekind  11121  zsupss  12659  uzwo3  12665  seqcl2  13722  seqcl  13724  seqf  13725  seqfveq2  13726  seqfveq  13728  seqshft2  13730  monoord  13734  monoord2  13735  sermono  13736  seqsplit  13737  seqcaopr3  13739  seqid  13749  seqid2  13750  seqhomo  13751  seqz  13752  discr1  13935  discr  13936  hashbclem  14145  wrdind  14416  limsupgre  15171  climi  15200  rlimi  15203  rlimclim1  15235  rlimclim  15236  climrlim2  15237  rlimcn1  15278  climcn1  15282  isercoll2  15361  caucvgrlem  15365  caucvgb  15372  iseraltlem2  15375  iseraltlem3  15376  fsumm1  15444  fsum1p  15446  fsumcom2  15467  fsumge1  15490  telfsumo  15495  telfsumo2  15496  fsumparts  15499  o1fsum  15506  isum1p  15534  isumnn0nn  15535  isumrpcl  15536  climcndslem1  15542  climcndslem2  15543  climcnds  15544  cvgrat  15576  mertenslem1  15577  mertens  15579  fprodm1  15658  fprod1p  15659  fprodcom2  15675  prmind2  16371  pcmpt2  16575  prmpwdvds  16586  prmreclem4  16601  prmreclem5  16602  vdwlem1  16663  vdwlem2  16664  vdwlem9  16671  vdwlem10  16672  rami  16697  ramcl  16711  prmodvdslcmf  16729  prmgaplcmlem1  16733  cshwsidrepsw  16776  prdsbasprj  17164  isacs2  17343  acsfiel  17344  catidex  17364  iscatd2  17371  catlid  17373  catrid  17374  subcidcl  17540  funcid  17566  yonedalem4c  17976  yonffthlem  17981  isdrs2  18005  luble  18058  glble  18071  joinle  18085  meetle  18099  poslubmo  18110  posglbmo  18111  acsdrsel  18242  isacs4lem  18243  isacs5lem  18244  acsdrscl  18245  acsficl  18246  lidrideqd  18334  grprinvlem  18338  grprinvd  18339  mndind  18447  grpidd2  18598  mulgsubcl  18699  issubg4  18755  ghmf1  18844  fislw  19211  efgsdmi  19319  efgsrel  19321  gexexlem  19434  gsumzaddlem  19503  gsummhm2  19521  dprdcntz  19592  dprddisj  19593  dprdss  19613  dprd2dlem2  19624  dprd2da  19626  dpjrid  19646  ablfac1eu  19657  pgpfac1lem1  19658  pgpfaclem2  19666  issrngd  20102  islbs2  20397  lbsextlem4  20404  prmirredlem  20675  psgndiflemB  20786  frlmphl  20969  mplsubglem  21186  mpllsslem  21187  subrgasclcl  21256  mplind  21259  evlslem1  21273  mdetralt  21738  mdetunilem1  21742  lmcvg  22394  iscncl  22401  lmff  22433  cnrmi  22492  cmpcov  22521  fiuncmp  22536  hauscmplem  22538  1stcfb  22577  1stcelcls  22593  restnlly  22614  islly2  22616  lly1stc  22628  kgeni  22669  ptpjpre1  22703  ptbasfi  22713  ptpjopn  22744  dfac14  22750  txtube  22772  cnmpt11  22795  cnmpt21  22803  cnmptkp  22812  cnmptk1p  22817  qtopomap  22850  qtopcmap  22851  flimcf  23114  fclscf  23157  flfcntr  23175  ptcmplem3  23186  tgpt0  23251  tsmsi  23266  tsmsxplem2  23286  tsmsxp  23287  isucn2  23412  ucnima  23414  ucncn  23418  cfiluweak  23428  cuspcvg  23434  imasdsf1olem  23507  lpbl  23640  comet  23650  cfilucfil  23696  cnheiborlem  24098  cnheibor  24099  bndth  24102  nmoleub2lem2  24260  nmoleub3  24263  ipcau2  24379  tcphcphlem1  24380  tcphcphlem2  24381  lmmcvg  24406  cmetcaulem  24433  iscmet3lem1  24436  iscmet3lem2  24437  pjthlem1  24582  pjthlem2  24583  ivthlem1  24596  ivthlem2  24597  ivthlem3  24598  ivth2  24600  ivthle  24601  ivthle2  24602  ivthicc  24603  ovoliunlem1  24647  ovolshftlem1  24654  ovolscalem1  24658  ovolicc2lem3  24664  ovolicc2lem4  24665  ovolicc2  24667  volsup  24701  dyadmbl  24745  vitalilem2  24754  vitalilem3  24755  mbfdm  24771  ismbf3d  24799  cncombf  24803  itg2seq  24888  itg2monolem2  24897  itg2monolem3  24898  itg2mono  24899  iblitg  24914  itgconst  24964  itgfsum  24972  limcvallem  25016  cnlimci  25034  cnmptlimc  25035  dvferm1lem  25129  dvferm1  25130  dvferm2lem  25131  dvferm2  25132  dvlipcn  25139  dvle  25152  lhop1lem  25158  dvfsumge  25167  dvfsumlem2  25172  dvfsumlem3  25173  ftc1a  25182  ftc1lem4  25184  itgsubstlem  25193  mdeglt  25211  deg1lt  25243  ply1divex  25282  fta1glem2  25312  fta1g  25313  plyco0  25334  plyeq0lem  25352  dgrcolem2  25416  plydivlem4  25437  plydivex  25438  fta1lem  25448  vieta1lem2  25452  vieta1  25453  tayl0  25502  ulmi  25526  ulmdvlem1  25540  ulmdvlem3  25542  ulmdv  25543  mtest  25544  pserulm  25562  efif1olem4  25682  rlimcnp  26096  rlimcnp2  26097  xrlimcnp  26099  scvxcvx  26116  lgamgulmlem5  26163  lgambdd  26167  lgamcvglem  26170  wilthlem2  26199  fsumdvdscom  26315  musumsum  26322  chtub  26341  fsumvma  26342  perfectlem2  26359  dchrelbas3  26367  dchrelbasd  26368  dchrn0  26379  dchrptlem2  26394  lgsval2lem  26436  lgsdirnn0  26473  lgsdinn0  26474  2sqlem10  26557  dchrisumlem1  26618  dchrmusum2  26623  dchrvmasumlem2  26627  dchrvmasumlem3  26628  dchrvmasumiflem1  26630  dchrisum0flblem2  26638  dchrisum0flb  26639  dchrisum0lem1b  26644  dchrisum0lem2  26647  2vmadivsumlem  26669  chpdifbndlem1  26682  selberg3lem1  26686  selberg4lem1  26689  pntrsumbnd2  26696  pntrlog2bndlem2  26707  pntrlog2bndlem3  26708  pntrlog2bndlem5  26710  pntrlog2bndlem6  26712  pntibndlem2  26720  pntibndlem3  26721  pntlemn  26729  pntlemj  26732  pntlemi  26733  pntlemo  26736  pntleme  26737  pntlem3  26738  pntlemp  26739  ostth2lem1  26747  ostthlem1  26756  ostth2lem2  26763  ostth3  26767  tglowdim1i  26843  tglowdim2ln  26993  wlkonl1iedg  28013  wlkp1lem7  28027  wlkp1lem8  28028  crctcshwlkn0lem6  28159  eupth2eucrct  28560  eupth2lem3  28579  ubthlem1  29211  ubthlem2  29212  minvecolem3  29217  occllem  29644  pjhthlem1  29732  wrdt2ind  31204  mgccole1  31247  mgcmnt2  31250  dfmgc2  31253  0nellinds  31545  linds2eq  31554  elrspunidl  31585  prmidl  31594  mxidlmax  31616  ssmxidl  31621  ply1scleq  31647  lbsdiflsp0  31686  fedgmullem1  31689  fedgmullem2  31690  extdg1id  31717  ofcfeqd2  32048  inelpisys  32101  unelldsys  32105  ldgenpisyslem1  32110  mbfmcnvima  32203  signstfvneq0  32530  fsum2dsub  32566  hgt750lemc  32606  hgt750lemd  32607  hgt749d  32608  hgt750lemf  32612  bnj1379  32789  bnj1450  33009  revwlk  33065  subfacp1lem5  33125  cvmlift2lem10  33253  frxp2  33770  frxp3  33776  nosupprefixmo  33882  noinfprefixmo  33883  noinfbnd1lem1  33905  noinfbnd1lem4  33908  noinfbnd2lem1  33912  noinfbnd2  33913  cofsslt  34067  coinitsslt  34068  unblimceq0lem  34665  unblimceq0  34666  unbdqndv2  34670  bj-ismoored  35257  lcmineqlem4  40020  dvle2  40060  aks4d1p9  40076  sticksstones1  40082  fnwe2lem2  40856  aomclem4  40862  scottelrankd  41818  mnuop123d  41833  mnuprdlem1  41843  mnuprdlem2  41844  eliind  42572  rnmptbd2lem  42747  rnmptbdlem  42754  limclner  43146  climisp  43241  climrescn  43243  climxrrelem  43244  climxrre  43245  cncfshift  43369  cncfperiod  43374  fperdvper  43414  salunicl  43811  saldifcl  43814  meadjuni  43949  lubsscl  46206  glbsscl  46207  ipolub  46226  ipoglb  46229  setcthin  46288