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  suppinisegdc  6513  tfrlem1  6584  tfrlem5  6590  tfr1onlemsucfn  6616  tfr1onlemsucaccv  6617  tfr1onlembxssdm  6619  tfr1onlembfn  6620  tfr1onlemaccex  6624  tfr1onlemres  6625  tfrcllemsucfn  6629  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllembfn  6633  tfrcllemaccex  6637  tfrcllemres  6638  tfrcl  6640  rdgon  6662  frecabcl  6675  pw2f1odclem  7140  elssdc  7215  undifdcss  7236  relresfin  7270  funisfsuppdc  7298  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  10062  irrmulap  10064  suprzubdc  10687  nninfdcex  10688  zsupssdc  10689  exbtwnzlemstep  10698  apbtwnz  10725  flaplt  10738  frecuzrdgsuc  10871  frecuzrdgg  10873  frecuzrdgsuctlem  10880  uzsinds  10901  iseqovex  10915  seq3val  10917  seqvalcd  10918  seq3-1  10919  seqf  10921  seq3p1  10922  seqovcd  10924  seqp1cd  10927  seq3clss  10928  seq3fveq2  10932  seqfveq2g  10934  seqfveqg  10935  seq3fveq  10936  seq3feq  10937  seq3shft2  10938  seqshft2g  10939  monoord  10942  monoord2  10943  ser3mono  10944  seq3split  10945  seqsplitg  10946  seq3caopr3  10948  seqcaopr3g  10949  iseqf1olemkle  10954  iseqf1olemklt  10955  iseqf1olemjpcl  10965  iseqf1olemqpcl  10966  iseqf1olemfvp  10967  seq3f1olemqsumkj  10968  seq3f1olemqsum  10970  seq3f1oleml  10973  seq3f1o  10974  seqf1og  10978  seq3id3  10981  seq3id  10982  seq3id2  10983  seq3homo  10984  seq3z  10985  seqhomog  10987  seqfeq4g  10988  ser3ge0  10993  nn0ltexp2  11168  hashfibclem  11303  zfz1isolemiso  11312  wrdind  11515  seq3shft  11624  cvg1nlemcau  11771  cvg1nlemres  11772  recvguniq  11782  resqrexlemgt0  11807  resqrexlemoverl  11808  resqrexlemglsq  11809  climi  12077  climcn1  12098  serf0  12142  fsum3cvg  12169  summodclem2  12173  summodc  12174  fsum3  12178  isumz  12180  fsumf1o  12181  isumss  12182  fisumss  12183  isumss2  12184  fsum3cvg2  12185  fsum3cvg3  12187  fsum3ser  12188  fsumsplit  12198  fsumm1  12207  fsum1p  12209  fisumcom2  12229  fsumge1  12252  telfsumo  12257  telfsumo2  12258  fsumparts  12261  isumshft  12281  isum1p  12283  isumnn0nn  12284  isumrpcl  12285  cvgratnnlemnexp  12315  cvgratnnlemmn  12316  cvgratnnlemseq  12317  cvgratnnlemabsle  12318  cvgratnnlemfm  12320  cvgratnnlemrate  12321  cvgratnn  12322  cvgratz  12323  mertenslemi1  12326  mertenslem2  12327  mertensabs  12328  fproddccvg  12363  prodmodclem2a  12367  prodmodc  12369  zproddc  12370  fprodseq  12374  prod1dc  12377  fprodf1o  12379  prodssdc  12380  fprodssdc  12381  fprodm1  12389  fprod1p  12390  fprodcom2fi  12417  sinltxirr  12552  bezoutlemmain  12799  bezoutlemex  12802  bezoutlemzz  12803  bezoutlemmo  12807  bezoutlemle  12809  bezoutlemsup  12810  nnmindc  12835  nnminle  12836  uzwodc  12838  nninfctlemfo  12841  prmind2  12922  isprm5lem  12944  isprm5  12945  pcmpt2  13151  prmpwdvds  13162  ennnfonelemk  13348  ennnfonelemex  13362  ennnfonelemnn0  13370  ctinfomlemom  13375  ctiunctlemudc  13385  ssnnctlemct  13394  nninfdclemcl  13396  nninfdclemp1  13398  nninfdc  13401  lidrideqd  13759  grpinvalem  13763  grpinva  13764  grpidd2  13904  mulgsubcl  13997  issubg4m  14054  ghmf1  14134  gzsummhm2  14235  gsumresfi  14262  gsummhm2fi  14264  gsum2dfilem2  14271  prdsbasprj  14288  lringuplu  14611  psrbaglefifi  15175  psrlidmfi  15208  psrridmfi  15209  icnpimaex  15454  lmcvg  15460  lmff  15492  cnmpt11  15526  cnmpt21  15534  comet  15742  dedekindeulemuub  15860  dedekindeulemloc  15862  dedekindeulemlu  15864  dedekindeulemeu  15865  suplociccreex  15867  suplociccex  15868  dedekindicclemuub  15869  dedekindicclemloc  15871  dedekindicclemlu  15873  dedekindicclemeu  15874  dedekindicc  15876  ivthinclemlopn  15879  ivthinclemlr  15880  ivthinclemuopn  15881  ivthinclemur  15882  ivthinclemdisj  15883  ivthinclemloc  15884  ivthinc  15886  ivthdec  15887  ivthreinc  15888  dich0  15895  limcimolemlt  15907  limcimo  15908  cnplimclemr  15912  cnlimci  15916  cnmptlimc  15917  limccnpcntop  15918  limccoap  15921  dvcoapbr  15950  eflt  16018  sin0pilem2  16026  pilem3  16027  chtqub  16313  perfectlem2  16317  lgsval2lem  16351  lgsdirnn0  16388  lgsdinn0  16389  2sqlem10  16466  eupth2lem3fi  16939  subctctexmid  17252  pw1nct  17255  exmidnotnotr  17258  exmidcon  17259  exmidpeirce  17260  nnsf  17271  nninfalllem1  17274  nninfsellemeqinf  17282  isomninnlem  17302  trilpolemlt1  17314  trirec0  17317  apdiff  17321  iswomninnlem  17323  ismkvnnlem  17326  redcwlpolemeq1  17328  redc0  17331  reap0  17332  cndcap  17333  dceqnconst  17334  dcapnconst  17335  nconstwlpolem0  17337  nconstwlpolem  17339  neap0mkv  17343  ltlenmkv  17344