Theorem rspcdva 2912

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395   ∈ wcel 2200  ∀wral 2508

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2801

This theorem is referenced by:  frirrg  4441  wetriext  4669  tfisi  4679  omsinds  4714  suppssov1  6221  caofref  6249  caofinvl  6250  caofdig  6258  oprssdmm  6323  tfrlem1  6460  tfrlem5  6466  tfr1onlemsucfn  6492  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfr1onlemaccex  6500  tfr1onlemres  6501  tfrcllemsucfn  6505  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllembfn  6509  tfrcllemaccex  6513  tfrcllemres  6514  tfrcl  6516  rdgon  6538  frecabcl  6551  pw2f1odclem  7003  elssdc  7075  undifdcss  7096  ctssdclemn0  7288  ctssdc  7291  nninfninc  7301  nnnninfeq  7306  nnnninfeq2  7307  enomnilem  7316  fodju0  7325  fodjuomnilemres  7326  ismkvnex  7333  fodjumkvlemres  7337  enmkvlem  7339  enwomnilem  7347  nninfdcinf  7349  nninfwlporlem  7351  nninfwlpoimlemdc  7355  nninfinfwlpolem  7356  exmidaclem  7401  exmidontriimlem4  7417  netap  7451  exmidapne  7457  cc2lem  7463  cc3  7465  prltlu  7685  cauappcvgprlemm  7843  caucvgprlemm  7866  caucvgprprlemml  7892  suplocexprlemmu  7916  suplocexprlemdisj  7918  suplocexprlemloc  7919  suplocexprlemub  7921  caucvgsrlemgt1  7993  caucvgsr  8000  suplocsrlemb  8004  suplocsrlempr  8005  suplocsrlem  8006  axcaucvglemcau  8096  axcaucvglemres  8097  axpre-suploclemres  8099  irrmulap  9855  suprzubdc  10468  nninfdcex  10469  zsupssdc  10470  exbtwnzlemstep  10479  apbtwnz  10506  frecuzrdgsuc  10648  frecuzrdgg  10650  frecuzrdgsuctlem  10657  uzsinds  10678  iseqovex  10692  seq3val  10694  seqvalcd  10695  seq3-1  10696  seqf  10698  seq3p1  10699  seqovcd  10701  seqp1cd  10704  seq3clss  10705  seq3fveq2  10709  seqfveq2g  10711  seqfveqg  10712  seq3fveq  10713  seq3feq  10714  seq3shft2  10715  seqshft2g  10716  monoord  10719  monoord2  10720  ser3mono  10721  seq3split  10722  seqsplitg  10723  seq3caopr3  10725  seqcaopr3g  10726  iseqf1olemkle  10731  iseqf1olemklt  10732  iseqf1olemjpcl  10742  iseqf1olemqpcl  10743  iseqf1olemfvp  10744  seq3f1olemqsumkj  10745  seq3f1olemqsum  10747  seq3f1oleml  10750  seq3f1o  10751  seqf1og  10755  seq3id3  10758  seq3id  10759  seq3id2  10760  seq3homo  10761  seq3z  10762  seqhomog  10764  seqfeq4g  10765  ser3ge0  10770  nn0ltexp2  10943  zfz1isolemiso  11074  wrdind  11269  seq3shft  11364  cvg1nlemcau  11510  cvg1nlemres  11511  recvguniq  11521  resqrexlemgt0  11546  resqrexlemoverl  11547  resqrexlemglsq  11548  climi  11813  climcn1  11834  serf0  11878  fsum3cvg  11904  summodclem2  11908  summodc  11909  fsum3  11913  isumz  11915  fsumf1o  11916  isumss  11917  fisumss  11918  isumss2  11919  fsum3cvg2  11920  fsum3cvg3  11922  fsum3ser  11923  fsumsplit  11933  fsumm1  11942  fsum1p  11944  fisumcom2  11964  fsumge1  11987  telfsumo  11992  telfsumo2  11993  fsumparts  11996  isumshft  12016  isum1p  12018  isumnn0nn  12019  isumrpcl  12020  cvgratnnlemnexp  12050  cvgratnnlemmn  12051  cvgratnnlemseq  12052  cvgratnnlemabsle  12053  cvgratnnlemfm  12055  cvgratnnlemrate  12056  cvgratnn  12057  cvgratz  12058  mertenslemi1  12061  mertenslem2  12062  mertensabs  12063  fproddccvg  12098  prodmodclem2a  12102  prodmodc  12104  zproddc  12105  fprodseq  12109  prod1dc  12112  fprodf1o  12114  prodssdc  12115  fprodssdc  12116  fprodm1  12124  fprod1p  12125  fprodcom2fi  12152  sinltxirr  12287  bezoutlemmain  12534  bezoutlemex  12537  bezoutlemzz  12538  bezoutlemmo  12542  bezoutlemle  12544  bezoutlemsup  12545  nnmindc  12570  nnminle  12571  uzwodc  12573  nninfctlemfo  12576  prmind2  12657  isprm5lem  12678  isprm5  12679  pcmpt2  12882  prmpwdvds  12893  ennnfonelemk  12986  ennnfonelemex  13000  ennnfonelemnn0  13008  ctinfomlemom  13013  ctiunctlemudc  13023  ssnnctlemct  13032  nninfdclemcl  13034  nninfdclemp1  13036  nninfdc  13039  prdsbasprj  13330  lidrideqd  13429  grpinvalem  13433  grpinva  13434  grpidd2  13589  mulgsubcl  13688  issubg4m  13745  ghmf1  13825  gsumfzmhm2  13896  lringuplu  14175  mplsubgfilemcl  14678  icnpimaex  14900  lmcvg  14906  lmff  14938  cnmpt11  14972  cnmpt21  14980  comet  15188  dedekindeulemuub  15306  dedekindeulemloc  15308  dedekindeulemlu  15310  dedekindeulemeu  15311  suplociccreex  15313  suplociccex  15314  dedekindicclemuub  15315  dedekindicclemloc  15317  dedekindicclemlu  15319  dedekindicclemeu  15320  dedekindicc  15322  ivthinclemlopn  15325  ivthinclemlr  15326  ivthinclemuopn  15327  ivthinclemur  15328  ivthinclemdisj  15329  ivthinclemloc  15330  ivthinc  15332  ivthdec  15333  ivthreinc  15334  dich0  15341  limcimolemlt  15353  limcimo  15354  cnplimclemr  15358  cnlimci  15362  cnmptlimc  15363  limccnpcntop  15364  limccoap  15367  dvcoapbr  15396  eflt  15464  sin0pilem2  15471  pilem3  15472  perfectlem2  15689  lgsval2lem  15704  lgsdirnn0  15741  lgsdinn0  15742  2sqlem10  15819  2omap  16418  subctctexmid  16425  pw1nct  16428  nnsf  16431  nninfalllem1  16434  nninfsellemeqinf  16442  isomninnlem  16458  trilpolemlt1  16469  trirec0  16472  apdiff  16476  iswomninnlem  16477  ismkvnnlem  16480  redcwlpolemeq1  16482  redc0  16485  reap0  16486  cndcap  16487  dceqnconst  16488  dcapnconst  16489  nconstwlpolem0  16491  nconstwlpolem  16493  neap0mkv  16497  ltlenmkv  16498