Theorem rspcdva 3625

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 208   = wceq 1537   ∈ wcel 2114  ∀wral 3138

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893  df-ral 3143

This theorem is referenced by:  nvocnv  7038  knatar  7110  caofref  7435  caofinvl  7436  tfisi  7573  suppssov1  7862  wfrlem17  7971  tfrlem1  8012  tfrlem5  8016  marypha1lem  8897  marypha1  8898  ordtypelem6  8987  ordtypelem7  8988  wemaplem2  9011  oemapvali  9147  cantnflem1c  9150  infxpenlem  9439  acni  9471  dfac9  9562  dfac12lem2  9570  sornom  9699  fin1ai  9715  fin2i  9717  fin23lem11  9739  isfin2-2  9741  fin23lem17  9760  fin23lem39  9772  fin1a2lem13  9834  hsmexlem4  9851  ttukeylem5  9935  ttukeylem6  9936  canth4  10069  pwfseqlem5  10085  winalim2  10118  wununi  10128  wunpw  10129  dedekind  10803  zsupss  12338  uzwo3  12344  seqcl2  13389  seqcl  13391  seqf  13392  seqfveq2  13393  seqfveq  13395  seqshft2  13397  monoord  13401  monoord2  13402  sermono  13403  seqsplit  13404  seqcaopr3  13406  seqid  13416  seqid2  13417  seqhomo  13418  seqz  13419  discr1  13601  discr  13602  hashbclem  13811  wrdind  14084  limsupgre  14838  climi  14867  rlimi  14870  rlimclim1  14902  rlimclim  14903  climrlim2  14904  rlimcn1  14945  climcn1  14948  isercoll2  15025  caucvgrlem  15029  caucvgb  15036  iseraltlem2  15039  iseraltlem3  15040  fsumm1  15106  fsum1p  15108  fsumcom2  15129  fsumge1  15152  telfsumo  15157  telfsumo2  15158  fsumparts  15161  o1fsum  15168  isum1p  15196  isumnn0nn  15197  isumrpcl  15198  climcndslem1  15204  climcndslem2  15205  climcnds  15206  cvgrat  15239  mertenslem1  15240  mertens  15242  fprodm1  15321  fprod1p  15322  fprodcom2  15338  prmind2  16029  pcmpt2  16229  prmpwdvds  16240  prmreclem4  16255  prmreclem5  16256  vdwlem1  16317  vdwlem2  16318  vdwlem9  16325  vdwlem10  16326  rami  16351  ramcl  16365  prmodvdslcmf  16383  prmgaplcmlem1  16387  cshwsidrepsw  16427  prdsbasprj  16745  isacs2  16924  acsfiel  16925  catidex  16945  iscatd2  16952  catlid  16954  catrid  16955  subcidcl  17114  funcid  17140  yonedalem4c  17527  yonffthlem  17532  isdrs2  17549  luble  17597  glble  17610  joinle  17624  meetle  17638  poslubmo  17756  posglbmo  17757  acsdrsel  17777  isacs4lem  17778  isacs5lem  17779  acsdrscl  17780  acsficl  17781  lidrideqd  17879  grprinvlem  17883  grprinvd  17884  mndind  17992  grpidd2  18141  mulgsubcl  18242  issubg4  18298  ghmf1  18387  fislw  18750  efgsdmi  18858  efgsrel  18860  gexexlem  18972  gsumzaddlem  19041  gsummhm2  19059  dprdcntz  19130  dprddisj  19131  dprdss  19151  dprd2dlem2  19162  dprd2da  19164  dpjrid  19184  ablfac1eu  19195  pgpfac1lem1  19196  pgpfaclem2  19204  issrngd  19632  islbs2  19926  lbsextlem4  19933  mplsubglem  20214  mpllsslem  20215  subrgasclcl  20279  mplind  20282  evlslem1  20295  prmirredlem  20640  psgndiflemB  20744  frlmphl  20925  mdetralt  21217  mdetunilem1  21221  lmcvg  21870  iscncl  21877  lmff  21909  cnrmi  21968  cmpcov  21997  fiuncmp  22012  hauscmplem  22014  1stcfb  22053  1stcelcls  22069  restnlly  22090  islly2  22092  lly1stc  22104  kgeni  22145  ptpjpre1  22179  ptbasfi  22189  ptpjopn  22220  dfac14  22226  txtube  22248  cnmpt11  22271  cnmpt21  22279  cnmptkp  22288  cnmptk1p  22293  qtopomap  22326  qtopcmap  22327  flimcf  22590  fclscf  22633  flfcntr  22651  ptcmplem3  22662  tgpt0  22727  tsmsi  22742  tsmsxplem2  22762  tsmsxp  22763  isucn2  22888  ucnima  22890  ucncn  22894  cfiluweak  22904  cuspcvg  22910  imasdsf1olem  22983  lpbl  23113  comet  23123  cfilucfil  23169  cnheiborlem  23558  cnheibor  23559  bndth  23562  nmoleub2lem2  23720  nmoleub3  23723  ipcau2  23837  tcphcphlem1  23838  tcphcphlem2  23839  lmmcvg  23864  cmetcaulem  23891  iscmet3lem1  23894  iscmet3lem2  23895  pjthlem1  24040  pjthlem2  24041  ivthlem1  24052  ivthlem2  24053  ivthlem3  24054  ivth2  24056  ivthle  24057  ivthle2  24058  ivthicc  24059  ovoliunlem1  24103  ovolshftlem1  24110  ovolscalem1  24114  ovolicc2lem3  24120  ovolicc2lem4  24121  ovolicc2  24123  volsup  24157  dyadmbl  24201  vitalilem2  24210  vitalilem3  24211  mbfdm  24227  ismbf3d  24255  cncombf  24259  itg2seq  24343  itg2monolem2  24352  itg2monolem3  24353  itg2mono  24354  iblitg  24369  itgconst  24419  itgfsum  24427  limcvallem  24469  cnlimci  24487  cnmptlimc  24488  dvferm1lem  24581  dvferm1  24582  dvferm2lem  24583  dvferm2  24584  dvlipcn  24591  dvle  24604  lhop1lem  24610  dvfsumge  24619  dvfsumlem2  24624  dvfsumlem3  24625  ftc1a  24634  ftc1lem4  24636  itgsubstlem  24645  mdeglt  24659  deg1lt  24691  ply1divex  24730  fta1glem2  24760  fta1g  24761  plyco0  24782  plyeq0lem  24800  dgrcolem2  24864  plydivlem4  24885  plydivex  24886  fta1lem  24896  vieta1lem2  24900  vieta1  24901  tayl0  24950  ulmi  24974  ulmdvlem1  24988  ulmdvlem3  24990  ulmdv  24991  mtest  24992  pserulm  25010  efif1olem4  25129  rlimcnp  25543  rlimcnp2  25544  xrlimcnp  25546  scvxcvx  25563  lgamgulmlem5  25610  lgambdd  25614  lgamcvglem  25617  wilthlem2  25646  fsumdvdscom  25762  musumsum  25769  chtub  25788  fsumvma  25789  perfectlem2  25806  dchrelbas3  25814  dchrelbasd  25815  dchrn0  25826  dchrptlem2  25841  lgsval2lem  25883  lgsdirnn0  25920  lgsdinn0  25921  2sqlem10  26004  dchrisumlem1  26065  dchrmusum2  26070  dchrvmasumlem2  26074  dchrvmasumlem3  26075  dchrvmasumiflem1  26077  dchrisum0flblem2  26085  dchrisum0flb  26086  dchrisum0lem1b  26091  dchrisum0lem2  26094  2vmadivsumlem  26116  chpdifbndlem1  26129  selberg3lem1  26133  selberg4lem1  26136  pntrsumbnd2  26143  pntrlog2bndlem2  26154  pntrlog2bndlem3  26155  pntrlog2bndlem5  26157  pntrlog2bndlem6  26159  pntibndlem2  26167  pntibndlem3  26168  pntlemn  26176  pntlemj  26179  pntlemi  26180  pntlemo  26183  pntleme  26184  pntlem3  26185  pntlemp  26186  ostth2lem1  26194  ostthlem1  26203  ostth2lem2  26210  ostth3  26214  tglowdim1i  26287  tglowdim2ln  26437  wlkonl1iedg  27447  wlkp1lem7  27461  wlkp1lem8  27462  crctcshwlkn0lem6  27593  eupth2eucrct  27996  eupth2lem3  28015  ubthlem1  28647  ubthlem2  28648  minvecolem3  28653  occllem  29080  pjhthlem1  29168  wrdt2ind  30627  0nellinds  30935  linds2eq  30941  prmidl  30957  mxidlmax  30974  ssmxidl  30979  lbsdiflsp0  31022  fedgmullem1  31025  fedgmullem2  31026  extdg1id  31053  ofcfeqd2  31360  inelpisys  31413  unelldsys  31417  ldgenpisyslem1  31422  mbfmcnvima  31515  signstfvneq0  31842  fsum2dsub  31878  hgt750lemc  31918  hgt750lemd  31919  hgt749d  31920  hgt750lemf  31924  bnj1379  32102  bnj1450  32322  revwlk  32371  cvmlift2lem10  32559  fpr3g  33122  unblimceq0lem  33845  unblimceq0  33846  unbdqndv2  33850  bj-ismoored  34402  fnwe2lem2  39671  aomclem4  39677  scottelrankd  40603  mnuop123d  40618  mnuprdlem1  40628  mnuprdlem2  40629  eliind  41353  rnmptbd2lem  41540  rnmptbdlem  41547  limclner  41952  climisp  42047  climrescn  42049  climxrrelem  42050  climxrre  42051  cncfshift  42177  cncfperiod  42182  fperdvper  42223  salunicl  42621  saldifcl  42624  meadjuni  42759