Theorem rspcdva 2916

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

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

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 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-v 2805

This theorem is referenced by:  frirrg  4453  wetriext  4681  tfisi  4691  omsinds  4726  suppssov1  6241  caofref  6269  caofinvl  6270  caofdig  6278  oprssdmm  6343  suppssdc  6438  suppssrst  6439  suppssrgst  6440  suppofss1dcl  6442  suppofss2dcl  6443  tfrlem1  6517  tfrlem5  6523  tfr1onlemsucfn  6549  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfr1onlemaccex  6557  tfr1onlemres  6558  tfrcllemsucfn  6562  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllembfn  6566  tfrcllemaccex  6570  tfrcllemres  6571  tfrcl  6573  rdgon  6595  frecabcl  6608  pw2f1odclem  7063  elssdc  7137  undifdcss  7158  ctssdclemn0  7352  ctssdc  7355  nninfninc  7365  nnnninfeq  7370  nnnninfeq2  7371  enomnilem  7380  fodju0  7389  fodjuomnilemres  7390  ismkvnex  7397  fodjumkvlemres  7401  enmkvlem  7403  enwomnilem  7411  nninfdcinf  7413  nninfwlporlem  7415  nninfwlpoimlemdc  7419  nninfinfwlpolem  7420  exmidaclem  7466  exmidontriimlem4  7482  netap  7516  exmidapne  7522  cc2lem  7528  cc3  7530  prltlu  7750  cauappcvgprlemm  7908  caucvgprlemm  7931  caucvgprprlemml  7957  suplocexprlemmu  7981  suplocexprlemdisj  7983  suplocexprlemloc  7984  suplocexprlemub  7986  caucvgsrlemgt1  8058  caucvgsr  8065  suplocsrlemb  8069  suplocsrlempr  8070  suplocsrlem  8071  axcaucvglemcau  8161  axcaucvglemres  8162  axpre-suploclemres  8164  irrmulap  9926  suprzubdc  10542  nninfdcex  10543  zsupssdc  10544  exbtwnzlemstep  10553  apbtwnz  10580  frecuzrdgsuc  10722  frecuzrdgg  10724  frecuzrdgsuctlem  10731  uzsinds  10752  iseqovex  10766  seq3val  10768  seqvalcd  10769  seq3-1  10770  seqf  10772  seq3p1  10773  seqovcd  10775  seqp1cd  10778  seq3clss  10779  seq3fveq2  10783  seqfveq2g  10785  seqfveqg  10786  seq3fveq  10787  seq3feq  10788  seq3shft2  10789  seqshft2g  10790  monoord  10793  monoord2  10794  ser3mono  10795  seq3split  10796  seqsplitg  10797  seq3caopr3  10799  seqcaopr3g  10800  iseqf1olemkle  10805  iseqf1olemklt  10806  iseqf1olemjpcl  10816  iseqf1olemqpcl  10817  iseqf1olemfvp  10818  seq3f1olemqsumkj  10819  seq3f1olemqsum  10821  seq3f1oleml  10824  seq3f1o  10825  seqf1og  10829  seq3id3  10832  seq3id  10833  seq3id2  10834  seq3homo  10835  seq3z  10836  seqhomog  10838  seqfeq4g  10839  ser3ge0  10844  nn0ltexp2  11017  zfz1isolemiso  11149  wrdind  11352  seq3shft  11461  cvg1nlemcau  11607  cvg1nlemres  11608  recvguniq  11618  resqrexlemgt0  11643  resqrexlemoverl  11644  resqrexlemglsq  11645  climi  11910  climcn1  11931  serf0  11975  fsum3cvg  12002  summodclem2  12006  summodc  12007  fsum3  12011  isumz  12013  fsumf1o  12014  isumss  12015  fisumss  12016  isumss2  12017  fsum3cvg2  12018  fsum3cvg3  12020  fsum3ser  12021  fsumsplit  12031  fsumm1  12040  fsum1p  12042  fisumcom2  12062  fsumge1  12085  telfsumo  12090  telfsumo2  12091  fsumparts  12094  isumshft  12114  isum1p  12116  isumnn0nn  12117  isumrpcl  12118  cvgratnnlemnexp  12148  cvgratnnlemmn  12149  cvgratnnlemseq  12150  cvgratnnlemabsle  12151  cvgratnnlemfm  12153  cvgratnnlemrate  12154  cvgratnn  12155  cvgratz  12156  mertenslemi1  12159  mertenslem2  12160  mertensabs  12161  fproddccvg  12196  prodmodclem2a  12200  prodmodc  12202  zproddc  12203  fprodseq  12207  prod1dc  12210  fprodf1o  12212  prodssdc  12213  fprodssdc  12214  fprodm1  12222  fprod1p  12223  fprodcom2fi  12250  sinltxirr  12385  bezoutlemmain  12632  bezoutlemex  12635  bezoutlemzz  12636  bezoutlemmo  12640  bezoutlemle  12642  bezoutlemsup  12643  nnmindc  12668  nnminle  12669  uzwodc  12671  nninfctlemfo  12674  prmind2  12755  isprm5lem  12776  isprm5  12777  pcmpt2  12980  prmpwdvds  12991  ennnfonelemk  13084  ennnfonelemex  13098  ennnfonelemnn0  13106  ctinfomlemom  13111  ctiunctlemudc  13121  ssnnctlemct  13130  nninfdclemcl  13132  nninfdclemp1  13134  nninfdc  13137  prdsbasprj  13428  lidrideqd  13527  grpinvalem  13531  grpinva  13532  grpidd2  13687  mulgsubcl  13786  issubg4m  13843  ghmf1  13923  gsumfzmhm2  13994  lringuplu  14274  mplsubgfilemcl  14783  icnpimaex  15005  lmcvg  15011  lmff  15043  cnmpt11  15077  cnmpt21  15085  comet  15293  dedekindeulemuub  15411  dedekindeulemloc  15413  dedekindeulemlu  15415  dedekindeulemeu  15416  suplociccreex  15418  suplociccex  15419  dedekindicclemuub  15420  dedekindicclemloc  15422  dedekindicclemlu  15424  dedekindicclemeu  15425  dedekindicc  15427  ivthinclemlopn  15430  ivthinclemlr  15431  ivthinclemuopn  15432  ivthinclemur  15433  ivthinclemdisj  15434  ivthinclemloc  15435  ivthinc  15437  ivthdec  15438  ivthreinc  15439  dich0  15446  limcimolemlt  15458  limcimo  15459  cnplimclemr  15463  cnlimci  15467  cnmptlimc  15468  limccnpcntop  15469  limccoap  15472  dvcoapbr  15501  eflt  15569  sin0pilem2  15576  pilem3  15577  perfectlem2  15797  lgsval2lem  15812  lgsdirnn0  15849  lgsdinn0  15850  2sqlem10  15927  eupth2lem3fi  16400  2omap  16698  subctctexmid  16705  pw1nct  16708  exmidnotnotr  16710  exmidcon  16711  exmidpeirce  16712  nnsf  16714  nninfalllem1  16717  nninfsellemeqinf  16725  isomninnlem  16745  trilpolemlt1  16756  trirec0  16759  apdiff  16763  iswomninnlem  16765  ismkvnnlem  16768  redcwlpolemeq1  16770  redc0  16773  reap0  16774  cndcap  16775  dceqnconst  16776  dcapnconst  16777  nconstwlpolem0  16779  nconstwlpolem  16781  neap0mkv  16785  ltlenmkv  16786