Theorem rspcdva 3517

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1601   ∈ wcel 2107  ∀wral 3090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-v 3400

This theorem is referenced by:  nvocnv  6809  knatar  6879  grprinvlem  7149  grprinvd  7150  caofref  7200  caofinvl  7201  tfisi  7336  suppssov1  7609  wfrlem17  7714  tfrlem1  7755  tfrlem5  7759  marypha1lem  8627  marypha1  8628  ordtypelem6  8717  ordtypelem7  8718  wemaplem2  8741  oemapvali  8878  cantnflem1c  8881  infxpenlem  9169  acni  9201  dfac9  9293  dfac12lem2  9301  sornom  9434  fin1ai  9450  fin2i  9452  fin23lem11  9474  isfin2-2  9476  fin23lem17  9495  fin23lem39  9507  fin1a2lem13  9569  hsmexlem4  9586  ttukeylem5  9670  ttukeylem6  9671  canth4  9804  pwfseqlem5  9820  winalim2  9853  wununi  9863  wunpw  9864  dedekind  10539  zsupss  12084  uzwo3  12090  seqcl2  13137  seqcl  13139  seqf  13140  seqfveq2  13141  seqfveq  13143  seqshft2  13145  monoord  13149  monoord2  13150  sermono  13151  seqsplit  13152  seqcaopr3  13154  seqid  13164  seqid2  13165  seqhomo  13166  seqz  13167  discr1  13319  discr  13320  hashbclem  13550  wrdind  13842  wrdindOLD  13843  limsupgre  14620  climi  14649  rlimi  14652  rlimclim1  14684  rlimclim  14685  climrlim2  14686  rlimcn1  14727  climcn1  14730  isercoll2  14807  caucvgrlem  14811  caucvgb  14818  iseraltlem2  14821  iseraltlem3  14822  fsumm1  14887  fsum1p  14889  fsumcom2  14910  fsumge1  14933  telfsumo  14938  telfsumo2  14939  fsumparts  14942  o1fsum  14949  isum1p  14977  isumnn0nn  14978  isumrpcl  14979  climcndslem1  14985  climcndslem2  14986  climcnds  14987  cvgrat  15018  mertenslem1  15019  mertens  15021  fprodm1  15100  fprod1p  15101  fprodcom2  15117  prmind2  15803  pcmpt2  16001  prmpwdvds  16012  prmreclem4  16027  prmreclem5  16028  vdwlem1  16089  vdwlem2  16090  vdwlem9  16097  vdwlem10  16098  rami  16123  ramcl  16137  prmodvdslcmf  16155  prmgaplcmlem1  16159  cshwsidrepsw  16199  prdsbasprj  16518  isacs2  16699  acsfiel  16700  catidex  16720  iscatd2  16727  catlid  16729  catrid  16730  subcidcl  16889  funcid  16915  yonedalem4c  17303  yonffthlem  17308  isdrs2  17325  luble  17373  glble  17386  joinle  17400  meetle  17414  poslubmo  17532  posglbmo  17533  acsdrsel  17553  isacs4lem  17554  isacs5lem  17555  acsdrscl  17556  acsficl  17557  mrcmndind  17752  grpidd2  17846  mulgsubcl  17942  issubg4  17997  ghmf1  18073  fislw  18424  efgsdmi  18529  efgsrel  18531  gexexlem  18641  gsumzaddlem  18707  gsummhm2  18725  dprdcntz  18794  dprddisj  18795  dprdss  18815  dprd2dlem2  18826  dprd2da  18828  dpjrid  18848  ablfac1eu  18859  pgpfac1lem1  18860  pgpfaclem2  18868  issrngd  19253  islbs2  19551  lbsextlem4  19558  mplsubglem  19831  mpllsslem  19832  subrgasclcl  19895  mplind  19898  evlslem1  19911  prmirredlem  20237  psgndiflemB  20342  frlmphl  20524  mdetralt  20819  mdetunilem1  20823  lmcvg  21474  iscncl  21481  lmff  21513  cnrmi  21572  cmpcov  21601  fiuncmp  21616  hauscmplem  21618  1stcfb  21657  1stcelcls  21673  restnlly  21694  islly2  21696  lly1stc  21708  kgeni  21749  ptpjpre1  21783  ptbasfi  21793  ptpjopn  21824  dfac14  21830  txtube  21852  cnmpt11  21875  cnmpt21  21883  cnmptkp  21892  cnmptk1p  21897  qtopomap  21930  qtopcmap  21931  flimcf  22194  fclscf  22237  flfcntr  22255  ptcmplem3  22266  tgpt0  22330  tsmsi  22345  tsmsxplem2  22365  tsmsxp  22366  isucn2  22491  ucnima  22493  ucncn  22497  cfiluweak  22507  cuspcvg  22513  imasdsf1olem  22586  lpbl  22716  comet  22726  cfilucfil  22772  cnheiborlem  23161  cnheibor  23162  bndth  23165  nmoleub2lem2  23323  nmoleub3  23326  ipcau2  23440  tcphcphlem1  23441  tcphcphlem2  23442  lmmcvg  23467  cmetcaulem  23494  iscmet3lem1  23497  iscmet3lem2  23498  pjthlem1  23643  pjthlem2  23644  ivthlem1  23655  ivthlem2  23656  ivthlem3  23657  ivth2  23659  ivthle  23660  ivthle2  23661  ivthicc  23662  ovoliunlem1  23706  ovolshftlem1  23713  ovolscalem1  23717  ovolicc2lem3  23723  ovolicc2lem4  23724  ovolicc2  23726  volsup  23760  dyadmbl  23804  vitalilem2  23813  vitalilem3  23814  mbfdm  23830  ismbf3d  23858  cncombf  23862  itg2seq  23946  itg2monolem2  23955  itg2monolem3  23956  itg2mono  23957  iblitg  23972  itgconst  24022  itgfsum  24030  limcvallem  24072  cnlimci  24090  cnmptlimc  24091  dvferm1lem  24184  dvferm1  24185  dvferm2lem  24186  dvferm2  24187  dvlipcn  24194  dvle  24207  lhop1lem  24213  dvfsumge  24222  dvfsumlem2  24227  dvfsumlem3  24228  ftc1a  24237  ftc1lem4  24239  itgsubstlem  24248  mdeglt  24262  deg1lt  24294  ply1divex  24333  fta1glem2  24363  fta1g  24364  plyco0  24385  plyeq0lem  24403  dgrcolem2  24467  plydivlem4  24488  plydivex  24489  fta1lem  24499  vieta1lem2  24503  vieta1  24504  tayl0  24553  ulmi  24577  ulmdvlem1  24591  ulmdvlem3  24593  ulmdv  24594  mtest  24595  pserulm  24613  efif1olem4  24729  rlimcnp  25144  rlimcnp2  25145  xrlimcnp  25147  scvxcvx  25164  lgamgulmlem5  25211  lgambdd  25215  lgamcvglem  25218  wilthlem2  25247  fsumdvdscom  25363  musumsum  25370  chtub  25389  fsumvma  25390  perfectlem2  25407  dchrelbas3  25415  dchrelbasd  25416  dchrn0  25427  dchrptlem2  25442  lgsval2lem  25484  lgsdirnn0  25521  lgsdinn0  25522  2sqlem10  25605  dchrisumlem1  25630  dchrmusum2  25635  dchrvmasumlem2  25639  dchrvmasumlem3  25640  dchrvmasumiflem1  25642  dchrisum0flblem2  25650  dchrisum0flb  25651  dchrisum0lem1b  25656  dchrisum0lem2  25659  2vmadivsumlem  25681  chpdifbndlem1  25694  selberg3lem1  25698  selberg4lem1  25701  pntrsumbnd2  25708  pntrlog2bndlem2  25719  pntrlog2bndlem3  25720  pntrlog2bndlem5  25722  pntrlog2bndlem6  25724  pntibndlem2  25732  pntibndlem3  25733  pntlemn  25741  pntlemj  25744  pntlemi  25745  pntlemo  25748  pntleme  25749  pntlem3  25750  pntlemp  25751  ostth2lem1  25759  ostthlem1  25768  ostth2lem2  25775  ostth3  25779  tglowdim1i  25852  tglowdim2ln  26002  wlkonl1iedg  27012  wlkp1lem7  27030  wlkp1lem8  27031  crctcshwlkn0lem6  27164  eupth2eucrct  27621  eupth2lem3  27640  ubthlem1  28298  ubthlem2  28299  minvecolem3  28304  occllem  28734  pjhthlem1  28822  0nellinds  30434  lbsdiflsp0  30440  inelpisys  30815  unelldsys  30819  ldgenpisyslem1  30824  fsum2dsub  31287  hgt750lemc  31327  hgt750lemd  31328  hgt749d  31329  hgt750lemf  31333  cvmlift2lem10  31893  unblimceq0lem  33079  unblimceq0  33080  unbdqndv2  33084  limclner  40791  climisp  40886  climrescn  40888  climxrrelem  40889  climxrre  40890  cncfshift  41015  cncfperiod  41020  fperdvper  41061  saldifcl  41463