Theorem rspcdva 3613

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062

This theorem is referenced by:  nvocnv  7275  knatar  7350  caofref  7695  caofinvl  7696  tfisi  7844  frxp2  8126  frxp3  8133  suppssov1  8179  fpr3g  8266  fprresex  8291  wfrlem17OLD  8321  tfrlem1  8372  tfrlem5  8376  coflton  8666  cofon1  8667  cofon2  8668  marypha1lem  9424  marypha1  9425  ordtypelem6  9514  ordtypelem7  9515  wemaplem2  9538  oemapvali  9675  cantnflem1c  9678  ttrcltr  9707  ttrclss  9711  dmttrcl  9712  rnttrcl  9713  ttrclselem2  9717  infxpenlem  10004  acni  10036  dfac9  10127  dfac12lem2  10135  sornom  10268  fin1ai  10284  fin2i  10286  fin23lem11  10308  isfin2-2  10310  fin23lem17  10329  fin23lem39  10341  fin1a2lem13  10403  hsmexlem4  10420  ttukeylem5  10504  ttukeylem6  10505  canth4  10638  pwfseqlem5  10654  winalim2  10687  wununi  10697  wunpw  10698  dedekind  11373  zsupss  12917  uzwo3  12923  seqcl2  13982  seqcl  13984  seqf  13985  seqfveq2  13986  seqfveq  13988  seqshft2  13990  monoord  13994  monoord2  13995  sermono  13996  seqsplit  13997  seqcaopr3  13999  seqid  14009  seqid2  14010  seqhomo  14011  seqz  14012  discr1  14198  discr  14199  hashbclem  14407  wrdind  14668  limsupgre  15421  climi  15450  rlimi  15453  rlimclim1  15485  rlimclim  15486  climrlim2  15487  rlimcn1  15528  climcn1  15532  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  15907  fprod1p  15908  fprodcom2  15924  prmind2  16618  pcmpt2  16822  prmpwdvds  16833  prmreclem4  16848  prmreclem5  16849  vdwlem1  16910  vdwlem2  16911  vdwlem9  16918  vdwlem10  16919  rami  16944  ramcl  16958  prmodvdslcmf  16976  prmgaplcmlem1  16980  cshwsidrepsw  17023  prdsbasprj  17414  isacs2  17593  acsfiel  17594  catidex  17614  iscatd2  17621  catlid  17623  catrid  17624  subcidcl  17790  funcid  17816  yonedalem4c  18226  yonffthlem  18231  isdrs2  18255  luble  18308  glble  18321  joinle  18335  meetle  18349  poslubmo  18360  posglbmo  18361  acsdrsel  18492  isacs4lem  18493  isacs5lem  18494  acsdrscl  18495  acsficl  18496  lidrideqd  18584  grprinvlem  18588  grpinva  18589  mndind  18705  grpidd2  18858  mulgsubcl  18962  issubg4  19019  ghmf1  19115  fislw  19487  efgsdmi  19594  efgsrel  19596  gexexlem  19714  gsumzaddlem  19783  gsummhm2  19801  dprdcntz  19872  dprddisj  19873  dprdss  19893  dprd2dlem2  19904  dprd2da  19906  dpjrid  19926  ablfac1eu  19937  pgpfac1lem1  19938  pgpfaclem2  19946  lringuplu  20306  issrngd  20461  islbs2  20759  lbsextlem4  20766  prmirredlem  21033  psgndiflemB  21144  frlmphl  21327  mplsubglem  21549  mpllsslem  21550  subrgasclcl  21619  mplind  21622  evlslem1  21636  mdetralt  22101  mdetunilem1  22105  lmcvg  22757  iscncl  22764  lmff  22796  cnrmi  22855  cmpcov  22884  fiuncmp  22899  hauscmplem  22901  1stcfb  22940  1stcelcls  22956  restnlly  22977  islly2  22979  lly1stc  22991  kgeni  23032  ptpjpre1  23066  ptbasfi  23076  ptpjopn  23107  dfac14  23113  txtube  23135  cnmpt11  23158  cnmpt21  23166  cnmptkp  23175  cnmptk1p  23180  qtopomap  23213  qtopcmap  23214  flimcf  23477  fclscf  23520  flfcntr  23538  ptcmplem3  23549  tgpt0  23614  tsmsi  23629  tsmsxplem2  23649  tsmsxp  23650  isucn2  23775  ucnima  23777  ucncn  23781  cfiluweak  23791  cuspcvg  23797  imasdsf1olem  23870  lpbl  24003  comet  24013  cfilucfil  24059  cnheiborlem  24461  cnheibor  24462  bndth  24465  nmoleub2lem2  24623  nmoleub3  24626  ipcau2  24742  tcphcphlem1  24743  tcphcphlem2  24744  lmmcvg  24769  cmetcaulem  24796  iscmet3lem1  24799  iscmet3lem2  24800  pjthlem1  24945  pjthlem2  24946  ivthlem1  24959  ivthlem2  24960  ivthlem3  24961  ivth2  24963  ivthle  24964  ivthle2  24965  ivthicc  24966  ovoliunlem1  25010  ovolshftlem1  25017  ovolscalem1  25021  ovolicc2lem3  25027  ovolicc2lem4  25028  ovolicc2  25030  volsup  25064  dyadmbl  25108  vitalilem2  25117  vitalilem3  25118  mbfdm  25134  ismbf3d  25162  cncombf  25166  itg2seq  25251  itg2monolem2  25260  itg2monolem3  25261  itg2mono  25262  iblitg  25277  itgconst  25327  itgfsum  25335  limcvallem  25379  cnlimci  25397  cnmptlimc  25398  dvferm1lem  25492  dvferm1  25493  dvferm2lem  25494  dvferm2  25495  dvlipcn  25502  dvle  25515  lhop1lem  25521  dvfsumge  25530  dvfsumlem2  25535  dvfsumlem3  25536  ftc1a  25545  ftc1lem4  25547  itgsubstlem  25556  mdeglt  25574  deg1lt  25606  ply1divex  25645  fta1glem2  25675  fta1g  25676  plyco0  25697  plyeq0lem  25715  dgrcolem2  25779  plydivlem4  25800  plydivex  25801  fta1lem  25811  vieta1lem2  25815  vieta1  25816  tayl0  25865  ulmi  25889  ulmdvlem1  25903  ulmdvlem3  25905  ulmdv  25906  mtest  25907  pserulm  25925  efif1olem4  26045  rlimcnp  26459  rlimcnp2  26460  xrlimcnp  26462  scvxcvx  26479  lgamgulmlem5  26526  lgambdd  26530  lgamcvglem  26533  wilthlem2  26562  fsumdvdscom  26678  musumsum  26685  chtub  26704  fsumvma  26705  perfectlem2  26722  dchrelbas3  26730  dchrelbasd  26731  dchrn0  26742  dchrptlem2  26757  lgsval2lem  26799  lgsdirnn0  26836  lgsdinn0  26837  2sqlem10  26920  dchrisumlem1  26981  dchrmusum2  26986  dchrvmasumlem2  26990  dchrvmasumlem3  26991  dchrvmasumiflem1  26993  dchrisum0flblem2  27001  dchrisum0flb  27002  dchrisum0lem1b  27007  dchrisum0lem2  27010  2vmadivsumlem  27032  chpdifbndlem1  27045  selberg3lem1  27049  selberg4lem1  27052  pntrsumbnd2  27059  pntrlog2bndlem2  27070  pntrlog2bndlem3  27071  pntrlog2bndlem5  27073  pntrlog2bndlem6  27075  pntibndlem2  27083  pntibndlem3  27084  pntlemn  27092  pntlemj  27095  pntlemi  27096  pntlemo  27099  pntleme  27100  pntlem3  27101  pntlemp  27102  ostth2lem1  27110  ostthlem1  27119  ostth2lem2  27126  ostth3  27130  nosupprefixmo  27192  noinfprefixmo  27193  noinfbnd1lem1  27215  noinfbnd1lem4  27218  noinfbnd2lem1  27222  noinfbnd2  27223  cofsslt  27394  coinitsslt  27395  sleadd1  27461  addsass  27477  negsid  27504  mulscom  27584  addsdilem3  27597  addsdilem4  27598  mulsasslem3  27609  precsexlem8  27649  precsexlem9  27650  precsexlem11  27652  tglowdim1i  27741  tglowdim2ln  27891  wlkonl1iedg  28911  wlkp1lem7  28925  wlkp1lem8  28926  crctcshwlkn0lem6  29058  eupth2eucrct  29459  eupth2lem3  29478  ubthlem1  30110  ubthlem2  30111  minvecolem3  30116  occllem  30543  pjhthlem1  30631  eqelbid  31702  wrdt2ind  32104  mgccole1  32147  mgcmnt2  32150  dfmgc2  32153  0nellinds  32471  linds2eq  32485  elrspunidl  32534  prmidl  32546  mxidlmax  32569  ssmxidl  32578  ply1scleq  32627  lbsdiflsp0  32699  fedgmullem1  32702  fedgmullem2  32703  extdg1id  32730  ofcfeqd2  33087  inelpisys  33140  unelldsys  33144  ldgenpisyslem1  33149  mbfmcnvima  33242  signstfvneq0  33571  fsum2dsub  33607  hgt750lemc  33647  hgt750lemd  33648  hgt749d  33649  hgt750lemf  33653  bnj1379  33829  bnj1450  34049  revwlk  34103  subfacp1lem5  34163  cvmlift2lem10  34291  gg-dvfsumlem2  35171  unblimceq0lem  35370  unblimceq0  35371  unbdqndv2  35375  bj-ismoored  35976  lcmineqlem4  40885  dvle2  40925  aks4d1p9  40941  sticksstones1  40950  fnwe2lem2  41778  aomclem4  41784  scottelrankd  42991  mnuop123d  43006  mnuprdlem1  43016  mnuprdlem2  43017  eliind  43743  rnmptbd2lem  43938  rnmptbdlem  43945  cvgcau  44187  limclner  44353  climisp  44448  climrescn  44450  climxrrelem  44451  climxrre  44452  cncfshift  44576  cncfperiod  44581  fperdvper  44621  salunicl  45018  saldifcl  45021  meadjuni  45159  lubsscl  47546  glbsscl  47547  ipolub  47566  ipoglb  47569  setcthin  47628