Theorem rspcdva 2928

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398   ∈ wcel 2205  ∀wral 2522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-v 2817

This theorem is referenced by:  frirrg  4476  wetriext  4704  tfisi  4714  omsinds  4749  suppssov1  6272  caofref  6300  caofinvl  6301  caofdig  6309  oprssdmm  6378  suppssdc  6473  suppssrst  6474  suppssrgst  6475  suppofss1dcl  6477  suppofss2dcl  6478  tfrlem1  6552  tfrlem5  6558  tfr1onlemsucfn  6584  tfr1onlemsucaccv  6585  tfr1onlembxssdm  6587  tfr1onlembfn  6588  tfr1onlemaccex  6592  tfr1onlemres  6593  tfrcllemsucfn  6597  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllembfn  6601  tfrcllemaccex  6605  tfrcllemres  6606  tfrcl  6608  rdgon  6630  frecabcl  6643  pw2f1odclem  7100  elssdc  7175  undifdcss  7196  2omap  7282  ctssdclemn0  7414  ctssdc  7417  nninfninc  7427  nnnninfeq  7432  nnnninfeq2  7433  enomnilem  7442  fodju0  7451  fodjuomnilemres  7452  ismkvnex  7459  fodjumkvlemres  7463  enmkvlem  7465  enwomnilem  7473  nninfdcinf  7475  nninfwlporlem  7477  nninfwlpoimlemdc  7481  nninfinfwlpolem  7482  exmidaclem  7528  exmidontriimlem4  7544  papirr  7575  papsym  7576  papcotr  7577  netap  7584  exmidapne  7590  cc2lem  7596  cc3  7598  prltlu  7818  cauappcvgprlemm  7976  caucvgprlemm  7999  caucvgprprlemml  8025  suplocexprlemmu  8049  suplocexprlemdisj  8051  suplocexprlemloc  8052  suplocexprlemub  8054  caucvgsrlemgt1  8126  caucvgsr  8133  suplocsrlemb  8137  suplocsrlempr  8138  suplocsrlem  8139  axcaucvglemcau  8229  axcaucvglemres  8230  axpre-suploclemres  8232  irrmulap  9998  suprzubdc  10620  nninfdcex  10621  zsupssdc  10622  exbtwnzlemstep  10631  apbtwnz  10658  frecuzrdgsuc  10800  frecuzrdgg  10802  frecuzrdgsuctlem  10809  uzsinds  10830  iseqovex  10844  seq3val  10846  seqvalcd  10847  seq3-1  10848  seqf  10850  seq3p1  10851  seqovcd  10853  seqp1cd  10856  seq3clss  10857  seq3fveq2  10861  seqfveq2g  10863  seqfveqg  10864  seq3fveq  10865  seq3feq  10866  seq3shft2  10867  seqshft2g  10868  monoord  10871  monoord2  10872  ser3mono  10873  seq3split  10874  seqsplitg  10875  seq3caopr3  10877  seqcaopr3g  10878  iseqf1olemkle  10883  iseqf1olemklt  10884  iseqf1olemjpcl  10894  iseqf1olemqpcl  10895  iseqf1olemfvp  10896  seq3f1olemqsumkj  10897  seq3f1olemqsum  10899  seq3f1oleml  10902  seq3f1o  10903  seqf1og  10907  seq3id3  10910  seq3id  10911  seq3id2  10912  seq3homo  10913  seq3z  10914  seqhomog  10916  seqfeq4g  10917  ser3ge0  10922  nn0ltexp2  11096  hashfibclem  11231  zfz1isolemiso  11236  wrdind  11439  seq3shft  11548  cvg1nlemcau  11694  cvg1nlemres  11695  recvguniq  11705  resqrexlemgt0  11730  resqrexlemoverl  11731  resqrexlemglsq  11732  climi  11997  climcn1  12018  serf0  12062  fsum3cvg  12089  summodclem2  12093  summodc  12094  fsum3  12098  isumz  12100  fsumf1o  12101  isumss  12102  fisumss  12103  isumss2  12104  fsum3cvg2  12105  fsum3cvg3  12107  fsum3ser  12108  fsumsplit  12118  fsumm1  12127  fsum1p  12129  fisumcom2  12149  fsumge1  12172  telfsumo  12177  telfsumo2  12178  fsumparts  12181  isumshft  12201  isum1p  12203  isumnn0nn  12204  isumrpcl  12205  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  cvgratnnlemseq  12237  cvgratnnlemabsle  12238  cvgratnnlemfm  12240  cvgratnnlemrate  12241  cvgratnn  12242  cvgratz  12243  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  fproddccvg  12283  prodmodclem2a  12287  prodmodc  12289  zproddc  12290  fprodseq  12294  prod1dc  12297  fprodf1o  12299  prodssdc  12300  fprodssdc  12301  fprodm1  12309  fprod1p  12310  fprodcom2fi  12337  sinltxirr  12472  bezoutlemmain  12719  bezoutlemex  12722  bezoutlemzz  12723  bezoutlemmo  12727  bezoutlemle  12729  bezoutlemsup  12730  nnmindc  12755  nnminle  12756  uzwodc  12758  nninfctlemfo  12761  prmind2  12842  isprm5lem  12863  isprm5  12864  pcmpt2  13067  prmpwdvds  13078  ennnfonelemk  13235  ennnfonelemex  13249  ennnfonelemnn0  13257  ctinfomlemom  13262  ctiunctlemudc  13272  ssnnctlemct  13281  nninfdclemcl  13283  nninfdclemp1  13285  nninfdc  13288  lidrideqd  13644  grpinvalem  13648  grpinva  13649  grpidd2  13796  mulgsubcl  13889  issubg4m  13946  ghmf1  14026  gsumfzmhm2  14097  prdsbasprj  14124  lringuplu  14441  mplsubgfilemcl  14980  icnpimaex  15202  lmcvg  15208  lmff  15240  cnmpt11  15274  cnmpt21  15282  comet  15490  dedekindeulemuub  15608  dedekindeulemloc  15610  dedekindeulemlu  15612  dedekindeulemeu  15613  suplociccreex  15615  suplociccex  15616  dedekindicclemuub  15617  dedekindicclemloc  15619  dedekindicclemlu  15621  dedekindicclemeu  15622  dedekindicc  15624  ivthinclemlopn  15627  ivthinclemlr  15628  ivthinclemuopn  15629  ivthinclemur  15630  ivthinclemdisj  15631  ivthinclemloc  15632  ivthinc  15634  ivthdec  15635  ivthreinc  15636  dich0  15643  limcimolemlt  15655  limcimo  15656  cnplimclemr  15660  cnlimci  15664  cnmptlimc  15665  limccnpcntop  15666  limccoap  15669  dvcoapbr  15698  eflt  15766  sin0pilem2  15773  pilem3  15774  perfectlem2  15994  lgsval2lem  16009  lgsdirnn0  16046  lgsdinn0  16047  2sqlem10  16124  eupth2lem3fi  16597  subctctexmid  16900  pw1nct  16903  exmidnotnotr  16905  exmidcon  16906  exmidpeirce  16907  nnsf  16909  nninfalllem1  16912  nninfsellemeqinf  16920  isomninnlem  16940  trilpolemlt1  16951  trirec0  16954  apdiff  16958  iswomninnlem  16960  ismkvnnlem  16963  redcwlpolemeq1  16965  redc0  16968  reap0  16969  cndcap  16970  trimul0or  16971  dceqnconst  16972  dcapnconst  16973  nconstwlpolem0  16975  nconstwlpolem  16977  neap0mkv  16981  ltlenmkv  16982