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  4497  wetriext  4726  tfisi  4736  omsinds  4771  suppssov1  6302  caofref  6331  caofinvl  6332  caofdig  6340  oprssdmm  6409  suppssdc  6504  suppssrst  6505  suppssrgst  6506  suppofss1dcl  6508  suppofss2dcl  6509  tfrlem1  6583  tfrlem5  6589  tfr1onlemsucfn  6615  tfr1onlemsucaccv  6616  tfr1onlembxssdm  6618  tfr1onlembfn  6619  tfr1onlemaccex  6623  tfr1onlemres  6624  tfrcllemsucfn  6628  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllembfn  6632  tfrcllemaccex  6636  tfrcllemres  6637  tfrcl  6639  rdgon  6661  frecabcl  6674  pw2f1odclem  7138  elssdc  7213  undifdcss  7234  relresfin  7268  2omap  7324  ctssdclemn0  7456  ctssdc  7459  nninfninc  7469  nnnninfeq  7474  nnnninfeq2  7475  enomnilem  7484  fodju0  7493  fodjuomnilemres  7494  ismkvnex  7501  fodjumkvlemres  7505  enmkvlem  7507  enwomnilem  7515  nninfdcinf  7517  nninfwlporlem  7519  nninfwlpoimlemdc  7523  nninfinfwlpolem  7524  exmidaclem  7570  exmidontriimlem4  7586  papirr  7617  papsym  7618  papcotr  7619  netap  7626  exmidapne  7632  cc2lem  7638  cc3  7640  prltlu  7860  cauappcvgprlemm  8018  caucvgprlemm  8041  caucvgprprlemml  8067  suplocexprlemmu  8091  suplocexprlemdisj  8093  suplocexprlemloc  8094  suplocexprlemub  8096  caucvgsrlemgt1  8168  caucvgsr  8175  suplocsrlemb  8179  suplocsrlempr  8180  suplocsrlem  8181  axcaucvglemcau  8271  axcaucvglemres  8272  axpre-suploclemres  8274  indfdc  9307  irraddap  10063  irrmulap  10065  suprzubdc  10688  nninfdcex  10689  zsupssdc  10690  exbtwnzlemstep  10699  apbtwnz  10726  flaplt  10739  frecuzrdgsuc  10872  frecuzrdgg  10874  frecuzrdgsuctlem  10881  uzsinds  10902  iseqovex  10916  seq3val  10918  seqvalcd  10919  seq3-1  10920  seqf  10922  seq3p1  10923  seqovcd  10925  seqp1cd  10928  seq3clss  10929  seq3fveq2  10933  seqfveq2g  10935  seqfveqg  10936  seq3fveq  10937  seq3feq  10938  seq3shft2  10939  seqshft2g  10940  monoord  10943  monoord2  10944  ser3mono  10945  seq3split  10946  seqsplitg  10947  seq3caopr3  10949  seqcaopr3g  10950  iseqf1olemkle  10955  iseqf1olemklt  10956  iseqf1olemjpcl  10966  iseqf1olemqpcl  10967  iseqf1olemfvp  10968  seq3f1olemqsumkj  10969  seq3f1olemqsum  10971  seq3f1oleml  10974  seq3f1o  10975  seqf1og  10979  seq3id3  10982  seq3id  10983  seq3id2  10984  seq3homo  10985  seq3z  10986  seqhomog  10988  seqfeq4g  10989  ser3ge0  10994  nn0ltexp2  11169  hashfibclem  11304  zfz1isolemiso  11313  wrdind  11516  seq3shft  11625  cvg1nlemcau  11772  cvg1nlemres  11773  recvguniq  11783  resqrexlemgt0  11808  resqrexlemoverl  11809  resqrexlemglsq  11810  climi  12078  climcn1  12099  serf0  12143  fsum3cvg  12170  summodclem2  12174  summodc  12175  fsum3  12179  isumz  12181  fsumf1o  12182  isumss  12183  fisumss  12184  isumss2  12185  fsum3cvg2  12186  fsum3cvg3  12188  fsum3ser  12189  fsumsplit  12199  fsumm1  12208  fsum1p  12210  fisumcom2  12230  fsumge1  12253  telfsumo  12258  telfsumo2  12259  fsumparts  12262  isumshft  12282  isum1p  12284  isumnn0nn  12285  isumrpcl  12286  cvgratnnlemnexp  12316  cvgratnnlemmn  12317  cvgratnnlemseq  12318  cvgratnnlemabsle  12319  cvgratnnlemfm  12321  cvgratnnlemrate  12322  cvgratnn  12323  cvgratz  12324  mertenslemi1  12327  mertenslem2  12328  mertensabs  12329  fproddccvg  12364  prodmodclem2a  12368  prodmodc  12370  zproddc  12371  fprodseq  12375  prod1dc  12378  fprodf1o  12380  prodssdc  12381  fprodssdc  12382  fprodm1  12390  fprod1p  12391  fprodcom2fi  12418  sinltxirr  12553  bezoutlemmain  12800  bezoutlemex  12803  bezoutlemzz  12804  bezoutlemmo  12808  bezoutlemle  12810  bezoutlemsup  12811  nnmindc  12836  nnminle  12837  uzwodc  12839  nninfctlemfo  12842  prmind2  12923  isprm5lem  12945  isprm5  12946  pcmpt2  13152  prmpwdvds  13163  ennnfonelemk  13349  ennnfonelemex  13363  ennnfonelemnn0  13371  ctinfomlemom  13376  ctiunctlemudc  13386  ssnnctlemct  13395  nninfdclemcl  13397  nninfdclemp1  13399  nninfdc  13402  lidrideqd  13760  grpinvalem  13764  grpinva  13765  grpidd2  13905  mulgsubcl  13998  issubg4m  14055  ghmf1  14135  gzsummhm2  14236  gsumresfi  14263  gsummhm2fi  14265  gsum2dfilem2  14272  prdsbasprj  14289  lringuplu  14612  psrbaglefifi  15172  psrlidmfi  15199  psrridmfi  15200  mplsubgfilemcl  15215  icnpimaex  15437  lmcvg  15443  lmff  15475  cnmpt11  15509  cnmpt21  15517  comet  15725  dedekindeulemuub  15843  dedekindeulemloc  15845  dedekindeulemlu  15847  dedekindeulemeu  15848  suplociccreex  15850  suplociccex  15851  dedekindicclemuub  15852  dedekindicclemloc  15854  dedekindicclemlu  15856  dedekindicclemeu  15857  dedekindicc  15859  ivthinclemlopn  15862  ivthinclemlr  15863  ivthinclemuopn  15864  ivthinclemur  15865  ivthinclemdisj  15866  ivthinclemloc  15867  ivthinc  15869  ivthdec  15870  ivthreinc  15871  dich0  15878  limcimolemlt  15890  limcimo  15891  cnplimclemr  15895  cnlimci  15899  cnmptlimc  15900  limccnpcntop  15901  limccoap  15904  dvcoapbr  15933  eflt  16001  sin0pilem2  16009  pilem3  16010  chtqub  16296  perfectlem2  16300  lgsval2lem  16334  lgsdirnn0  16371  lgsdinn0  16372  2sqlem10  16449  eupth2lem3fi  16922  subctctexmid  17235  pw1nct  17238  exmidnotnotr  17241  exmidcon  17242  exmidpeirce  17243  nnsf  17254  nninfalllem1  17257  nninfsellemeqinf  17265  isomninnlem  17285  trilpolemlt1  17297  trirec0  17300  apdiff  17304  iswomninnlem  17306  ismkvnnlem  17309  redcwlpolemeq1  17311  redc0  17314  reap0  17315  cndcap  17316  dceqnconst  17317  dcapnconst  17318  nconstwlpolem0  17320  nconstwlpolem  17322  neap0mkv  17326  ltlenmkv  17327