Theorem rspcdva 2934

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-v 2823

This theorem is used by:  frirrg  4495  wetriext  4724  tfisi  4734  omsinds  4769  suppssov1  6299  caofref  6327  caofinvl  6328  caofdig  6336  oprssdmm  6405  suppssdc  6500  suppssrst  6501  suppssrgst  6502  suppofss1dcl  6504  suppofss2dcl  6505  tfrlem1  6579  tfrlem5  6585  tfr1onlemsucfn  6611  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemaccex  6619  tfr1onlemres  6620  tfrcllemsucfn  6624  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemaccex  6632  tfrcllemres  6633  tfrcl  6635  rdgon  6657  frecabcl  6670  pw2f1odclem  7134  elssdc  7209  undifdcss  7230  2omap  7319  ctssdclemn0  7451  ctssdc  7454  nninfninc  7464  nnnninfeq  7469  nnnninfeq2  7470  enomnilem  7479  fodju0  7488  fodjuomnilemres  7489  ismkvnex  7496  fodjumkvlemres  7500  enmkvlem  7502  enwomnilem  7510  nninfdcinf  7512  nninfwlporlem  7514  nninfwlpoimlemdc  7518  nninfinfwlpolem  7519  exmidaclem  7565  exmidontriimlem4  7581  papirr  7612  papsym  7613  papcotr  7614  netap  7621  exmidapne  7627  cc2lem  7633  cc3  7635  prltlu  7855  cauappcvgprlemm  8013  caucvgprlemm  8036  caucvgprprlemml  8062  suplocexprlemmu  8086  suplocexprlemdisj  8088  suplocexprlemloc  8089  suplocexprlemub  8091  caucvgsrlemgt1  8163  caucvgsr  8170  suplocsrlemb  8174  suplocsrlempr  8175  suplocsrlem  8176  axcaucvglemcau  8266  axcaucvglemres  8267  axpre-suploclemres  8269  indfdc  9301  irraddap  10057  irrmulap  10059  suprzubdc  10682  nninfdcex  10683  zsupssdc  10684  exbtwnzlemstep  10693  apbtwnz  10720  flaplt  10733  frecuzrdgsuc  10866  frecuzrdgg  10868  frecuzrdgsuctlem  10875  uzsinds  10896  iseqovex  10910  seq3val  10912  seqvalcd  10913  seq3-1  10914  seqf  10916  seq3p1  10917  seqovcd  10919  seqp1cd  10922  seq3clss  10923  seq3fveq2  10927  seqfveq2g  10929  seqfveqg  10930  seq3fveq  10931  seq3feq  10932  seq3shft2  10933  seqshft2g  10934  monoord  10937  monoord2  10938  ser3mono  10939  seq3split  10940  seqsplitg  10941  seq3caopr3  10943  seqcaopr3g  10944  iseqf1olemkle  10949  iseqf1olemklt  10950  iseqf1olemjpcl  10960  iseqf1olemqpcl  10961  iseqf1olemfvp  10962  seq3f1olemqsumkj  10963  seq3f1olemqsum  10965  seq3f1oleml  10968  seq3f1o  10969  seqf1og  10973  seq3id3  10976  seq3id  10977  seq3id2  10978  seq3homo  10979  seq3z  10980  seqhomog  10982  seqfeq4g  10983  ser3ge0  10988  nn0ltexp2  11163  hashfibclem  11298  zfz1isolemiso  11307  wrdind  11510  seq3shft  11619  cvg1nlemcau  11766  cvg1nlemres  11767  recvguniq  11777  resqrexlemgt0  11802  resqrexlemoverl  11803  resqrexlemglsq  11804  climi  12072  climcn1  12093  serf0  12137  fsum3cvg  12164  summodclem2  12168  summodc  12169  fsum3  12173  isumz  12175  fsumf1o  12176  isumss  12177  fisumss  12178  isumss2  12179  fsum3cvg2  12180  fsum3cvg3  12182  fsum3ser  12183  fsumsplit  12193  fsumm1  12202  fsum1p  12204  fisumcom2  12224  fsumge1  12247  telfsumo  12252  telfsumo2  12253  fsumparts  12256  isumshft  12276  isum1p  12278  isumnn0nn  12279  isumrpcl  12280  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  cvgratnnlemseq  12312  cvgratnnlemabsle  12313  cvgratnnlemfm  12315  cvgratnnlemrate  12316  cvgratnn  12317  cvgratz  12318  mertenslemi1  12321  mertenslem2  12322  mertensabs  12323  fproddccvg  12358  prodmodclem2a  12362  prodmodc  12364  zproddc  12365  fprodseq  12369  prod1dc  12372  fprodf1o  12374  prodssdc  12375  fprodssdc  12376  fprodm1  12384  fprod1p  12385  fprodcom2fi  12412  sinltxirr  12547  bezoutlemmain  12794  bezoutlemex  12797  bezoutlemzz  12798  bezoutlemmo  12802  bezoutlemle  12804  bezoutlemsup  12805  nnmindc  12830  nnminle  12831  uzwodc  12833  nninfctlemfo  12836  prmind2  12917  isprm5lem  12939  isprm5  12940  pcmpt2  13146  prmpwdvds  13157  ennnfonelemk  13343  ennnfonelemex  13357  ennnfonelemnn0  13365  ctinfomlemom  13370  ctiunctlemudc  13380  ssnnctlemct  13389  nninfdclemcl  13391  nninfdclemp1  13393  nninfdc  13396  lidrideqd  13754  grpinvalem  13758  grpinva  13759  grpidd2  13899  mulgsubcl  13992  issubg4m  14049  ghmf1  14129  gzsummhm2  14230  gsummhm2fi  14249  prdsbasprj  14266  lringuplu  14587  psrbaglefifi  15147  mplsubgfilemcl  15181  icnpimaex  15403  lmcvg  15409  lmff  15441  cnmpt11  15475  cnmpt21  15483  comet  15691  dedekindeulemuub  15809  dedekindeulemloc  15811  dedekindeulemlu  15813  dedekindeulemeu  15814  suplociccreex  15816  suplociccex  15817  dedekindicclemuub  15818  dedekindicclemloc  15820  dedekindicclemlu  15822  dedekindicclemeu  15823  dedekindicc  15825  ivthinclemlopn  15828  ivthinclemlr  15829  ivthinclemuopn  15830  ivthinclemur  15831  ivthinclemdisj  15832  ivthinclemloc  15833  ivthinc  15835  ivthdec  15836  ivthreinc  15837  dich0  15844  limcimolemlt  15856  limcimo  15857  cnplimclemr  15861  cnlimci  15865  cnmptlimc  15866  limccnpcntop  15867  limccoap  15870  dvcoapbr  15899  eflt  15967  sin0pilem2  15975  pilem3  15976  chtqub  16257  perfectlem2  16261  lgsval2lem  16295  lgsdirnn0  16332  lgsdinn0  16333  2sqlem10  16410  eupth2lem3fi  16883  subctctexmid  17196  pw1nct  17199  exmidnotnotr  17202  exmidcon  17203  exmidpeirce  17204  nnsf  17214  nninfalllem1  17217  nninfsellemeqinf  17225  isomninnlem  17245  trilpolemlt1  17257  trirec0  17260  apdiff  17264  iswomninnlem  17266  ismkvnnlem  17269  redcwlpolemeq1  17271  redc0  17274  reap0  17275  cndcap  17276  dceqnconst  17277  dcapnconst  17278  nconstwlpolem0  17280  nconstwlpolem  17282  neap0mkv  17286  ltlenmkv  17287