Theorem rspcdva 2869

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364   ∈ wcel 2164  ∀wral 2472

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-v 2762

This theorem is referenced by:  frirrg  4381  wetriext  4609  tfisi  4619  omsinds  4654  suppssov1  6127  caofref  6154  caofinvl  6155  caofdig  6159  oprssdmm  6224  tfrlem1  6361  tfrlem5  6367  tfr1onlemsucfn  6393  tfr1onlemsucaccv  6394  tfr1onlembxssdm  6396  tfr1onlembfn  6397  tfr1onlemaccex  6401  tfr1onlemres  6402  tfrcllemsucfn  6406  tfrcllemsucaccv  6407  tfrcllembxssdm  6409  tfrcllembfn  6410  tfrcllemaccex  6414  tfrcllemres  6415  tfrcl  6417  rdgon  6439  frecabcl  6452  pw2f1odclem  6890  undifdcss  6979  ctssdclemn0  7169  ctssdc  7172  nninfninc  7182  nnnninfeq  7187  nnnninfeq2  7188  enomnilem  7197  fodju0  7206  fodjuomnilemres  7207  ismkvnex  7214  fodjumkvlemres  7218  enmkvlem  7220  enwomnilem  7228  nninfdcinf  7230  nninfwlporlem  7232  nninfwlpoimlemdc  7236  exmidaclem  7268  exmidontriimlem4  7284  netap  7314  exmidapne  7320  cc2lem  7326  cc3  7328  prltlu  7547  cauappcvgprlemm  7705  caucvgprlemm  7728  caucvgprprlemml  7754  suplocexprlemmu  7778  suplocexprlemdisj  7780  suplocexprlemloc  7781  suplocexprlemub  7783  caucvgsrlemgt1  7855  caucvgsr  7862  suplocsrlemb  7866  suplocsrlempr  7867  suplocsrlem  7868  axcaucvglemcau  7958  axcaucvglemres  7959  axpre-suploclemres  7961  irrmulap  9713  exbtwnzlemstep  10316  apbtwnz  10343  frecuzrdgsuc  10485  frecuzrdgg  10487  frecuzrdgsuctlem  10494  uzsinds  10515  iseqovex  10529  seq3val  10531  seqvalcd  10532  seq3-1  10533  seqf  10535  seq3p1  10536  seqovcd  10538  seqp1cd  10541  seq3clss  10542  seq3fveq2  10546  seqfveq2g  10548  seqfveqg  10549  seq3fveq  10550  seq3feq  10551  seq3shft2  10552  seqshft2g  10553  monoord  10556  monoord2  10557  ser3mono  10558  seq3split  10559  seqsplitg  10560  seq3caopr3  10562  seqcaopr3g  10563  iseqf1olemkle  10568  iseqf1olemklt  10569  iseqf1olemjpcl  10579  iseqf1olemqpcl  10580  iseqf1olemfvp  10581  seq3f1olemqsumkj  10582  seq3f1olemqsum  10584  seq3f1oleml  10587  seq3f1o  10588  seqf1og  10592  seq3id3  10595  seq3id  10596  seq3id2  10597  seq3homo  10598  seq3z  10599  seqhomog  10601  seqfeq4g  10602  ser3ge0  10607  nn0ltexp2  10780  zfz1isolemiso  10910  seq3shft  10982  cvg1nlemcau  11128  cvg1nlemres  11129  recvguniq  11139  resqrexlemgt0  11164  resqrexlemoverl  11165  resqrexlemglsq  11166  climi  11430  climcn1  11451  serf0  11495  fsum3cvg  11521  summodclem2  11525  summodc  11526  fsum3  11530  isumz  11532  fsumf1o  11533  isumss  11534  fisumss  11535  isumss2  11536  fsum3cvg2  11537  fsum3cvg3  11539  fsum3ser  11540  fsumsplit  11550  fsumm1  11559  fsum1p  11561  fisumcom2  11581  fsumge1  11604  telfsumo  11609  telfsumo2  11610  fsumparts  11613  isumshft  11633  isum1p  11635  isumnn0nn  11636  isumrpcl  11637  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  cvgratnnlemseq  11669  cvgratnnlemabsle  11670  cvgratnnlemfm  11672  cvgratnnlemrate  11673  cvgratnn  11674  cvgratz  11675  mertenslemi1  11678  mertenslem2  11679  mertensabs  11680  fproddccvg  11715  prodmodclem2a  11719  prodmodc  11721  zproddc  11722  fprodseq  11726  prod1dc  11729  fprodf1o  11731  prodssdc  11732  fprodssdc  11733  fprodm1  11741  fprod1p  11742  fprodcom2fi  11769  sinltxirr  11904  suprzubdc  12089  nninfdcex  12090  zsupssdc  12091  bezoutlemmain  12135  bezoutlemex  12138  bezoutlemzz  12139  bezoutlemmo  12143  bezoutlemle  12145  bezoutlemsup  12146  nnmindc  12171  nnminle  12172  uzwodc  12174  nninfctlemfo  12177  prmind2  12258  isprm5lem  12279  isprm5  12280  pcmpt2  12482  prmpwdvds  12493  ennnfonelemk  12557  ennnfonelemex  12571  ennnfonelemnn0  12579  ctinfomlemom  12584  ctiunctlemudc  12594  ssnnctlemct  12603  nninfdclemcl  12605  nninfdclemp1  12607  nninfdc  12610  lidrideqd  12964  grpinvalem  12968  grpinva  12969  grpidd2  13113  mulgsubcl  13206  issubg4m  13263  ghmf1  13343  gsumfzmhm2  13414  lringuplu  13692  icnpimaex  14379  lmcvg  14385  lmff  14417  cnmpt11  14451  cnmpt21  14459  comet  14667  dedekindeulemuub  14771  dedekindeulemloc  14773  dedekindeulemlu  14775  dedekindeulemeu  14776  suplociccreex  14778  suplociccex  14779  dedekindicclemuub  14780  dedekindicclemloc  14782  dedekindicclemlu  14784  dedekindicclemeu  14785  dedekindicc  14787  ivthinclemlopn  14790  ivthinclemlr  14791  ivthinclemuopn  14792  ivthinclemur  14793  ivthinclemdisj  14794  ivthinclemloc  14795  ivthinc  14797  ivthdec  14798  ivthreinc  14799  dich0  14806  limcimolemlt  14818  limcimo  14819  cnplimclemr  14823  cnlimci  14827  cnmptlimc  14828  limccnpcntop  14829  limccoap  14832  dvcoapbr  14856  eflt  14910  sin0pilem2  14917  pilem3  14918  lgsval2lem  15126  lgsdirnn0  15163  lgsdinn0  15164  2sqlem10  15212  subctctexmid  15491  pw1nct  15493  nnsf  15495  nninfalllem1  15498  nninfsellemeqinf  15506  isomninnlem  15520  trilpolemlt1  15531  trirec0  15534  apdiff  15538  iswomninnlem  15539  ismkvnnlem  15542  redcwlpolemeq1  15544  redc0  15547  reap0  15548  cndcap  15549  dceqnconst  15550  dcapnconst  15551  nconstwlpolem0  15553  nconstwlpolem  15555  neap0mkv  15559  ltlenmkv  15560