Theorem rspcdva 2886

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373   ∈ wcel 2177  ∀wral 2485

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-v 2775

This theorem is referenced by:  frirrg  4404  wetriext  4632  tfisi  4642  omsinds  4677  suppssov1  6167  caofref  6195  caofinvl  6196  caofdig  6204  oprssdmm  6269  tfrlem1  6406  tfrlem5  6412  tfr1onlemsucfn  6438  tfr1onlemsucaccv  6439  tfr1onlembxssdm  6441  tfr1onlembfn  6442  tfr1onlemaccex  6446  tfr1onlemres  6447  tfrcllemsucfn  6451  tfrcllemsucaccv  6452  tfrcllembxssdm  6454  tfrcllembfn  6455  tfrcllemaccex  6459  tfrcllemres  6460  tfrcl  6462  rdgon  6484  frecabcl  6497  pw2f1odclem  6945  undifdcss  7034  ctssdclemn0  7226  ctssdc  7229  nninfninc  7239  nnnninfeq  7244  nnnninfeq2  7245  enomnilem  7254  fodju0  7263  fodjuomnilemres  7264  ismkvnex  7271  fodjumkvlemres  7275  enmkvlem  7277  enwomnilem  7285  nninfdcinf  7287  nninfwlporlem  7289  nninfwlpoimlemdc  7293  nninfinfwlpolem  7294  exmidaclem  7335  exmidontriimlem4  7351  netap  7381  exmidapne  7387  cc2lem  7393  cc3  7395  prltlu  7615  cauappcvgprlemm  7773  caucvgprlemm  7796  caucvgprprlemml  7822  suplocexprlemmu  7846  suplocexprlemdisj  7848  suplocexprlemloc  7849  suplocexprlemub  7851  caucvgsrlemgt1  7923  caucvgsr  7930  suplocsrlemb  7934  suplocsrlempr  7935  suplocsrlem  7936  axcaucvglemcau  8026  axcaucvglemres  8027  axpre-suploclemres  8029  irrmulap  9784  suprzubdc  10396  nninfdcex  10397  zsupssdc  10398  exbtwnzlemstep  10407  apbtwnz  10434  frecuzrdgsuc  10576  frecuzrdgg  10578  frecuzrdgsuctlem  10585  uzsinds  10606  iseqovex  10620  seq3val  10622  seqvalcd  10623  seq3-1  10624  seqf  10626  seq3p1  10627  seqovcd  10629  seqp1cd  10632  seq3clss  10633  seq3fveq2  10637  seqfveq2g  10639  seqfveqg  10640  seq3fveq  10641  seq3feq  10642  seq3shft2  10643  seqshft2g  10644  monoord  10647  monoord2  10648  ser3mono  10649  seq3split  10650  seqsplitg  10651  seq3caopr3  10653  seqcaopr3g  10654  iseqf1olemkle  10659  iseqf1olemklt  10660  iseqf1olemjpcl  10670  iseqf1olemqpcl  10671  iseqf1olemfvp  10672  seq3f1olemqsumkj  10673  seq3f1olemqsum  10675  seq3f1oleml  10678  seq3f1o  10679  seqf1og  10683  seq3id3  10686  seq3id  10687  seq3id2  10688  seq3homo  10689  seq3z  10690  seqhomog  10692  seqfeq4g  10693  ser3ge0  10698  nn0ltexp2  10871  zfz1isolemiso  11001  wrdind  11193  seq3shft  11219  cvg1nlemcau  11365  cvg1nlemres  11366  recvguniq  11376  resqrexlemgt0  11401  resqrexlemoverl  11402  resqrexlemglsq  11403  climi  11668  climcn1  11689  serf0  11733  fsum3cvg  11759  summodclem2  11763  summodc  11764  fsum3  11768  isumz  11770  fsumf1o  11771  isumss  11772  fisumss  11773  isumss2  11774  fsum3cvg2  11775  fsum3cvg3  11777  fsum3ser  11778  fsumsplit  11788  fsumm1  11797  fsum1p  11799  fisumcom2  11819  fsumge1  11842  telfsumo  11847  telfsumo2  11848  fsumparts  11851  isumshft  11871  isum1p  11873  isumnn0nn  11874  isumrpcl  11875  cvgratnnlemnexp  11905  cvgratnnlemmn  11906  cvgratnnlemseq  11907  cvgratnnlemabsle  11908  cvgratnnlemfm  11910  cvgratnnlemrate  11911  cvgratnn  11912  cvgratz  11913  mertenslemi1  11916  mertenslem2  11917  mertensabs  11918  fproddccvg  11953  prodmodclem2a  11957  prodmodc  11959  zproddc  11960  fprodseq  11964  prod1dc  11967  fprodf1o  11969  prodssdc  11970  fprodssdc  11971  fprodm1  11979  fprod1p  11980  fprodcom2fi  12007  sinltxirr  12142  bezoutlemmain  12389  bezoutlemex  12392  bezoutlemzz  12393  bezoutlemmo  12397  bezoutlemle  12399  bezoutlemsup  12400  nnmindc  12425  nnminle  12426  uzwodc  12428  nninfctlemfo  12431  prmind2  12512  isprm5lem  12533  isprm5  12534  pcmpt2  12737  prmpwdvds  12748  ennnfonelemk  12841  ennnfonelemex  12855  ennnfonelemnn0  12863  ctinfomlemom  12868  ctiunctlemudc  12878  ssnnctlemct  12887  nninfdclemcl  12889  nninfdclemp1  12891  nninfdc  12894  prdsbasprj  13184  lidrideqd  13283  grpinvalem  13287  grpinva  13288  grpidd2  13443  mulgsubcl  13542  issubg4m  13599  ghmf1  13679  gsumfzmhm2  13750  lringuplu  14028  mplsubgfilemcl  14531  icnpimaex  14753  lmcvg  14759  lmff  14791  cnmpt11  14825  cnmpt21  14833  comet  15041  dedekindeulemuub  15159  dedekindeulemloc  15161  dedekindeulemlu  15163  dedekindeulemeu  15164  suplociccreex  15166  suplociccex  15167  dedekindicclemuub  15168  dedekindicclemloc  15170  dedekindicclemlu  15172  dedekindicclemeu  15173  dedekindicc  15175  ivthinclemlopn  15178  ivthinclemlr  15179  ivthinclemuopn  15180  ivthinclemur  15181  ivthinclemdisj  15182  ivthinclemloc  15183  ivthinc  15185  ivthdec  15186  ivthreinc  15187  dich0  15194  limcimolemlt  15206  limcimo  15207  cnplimclemr  15211  cnlimci  15215  cnmptlimc  15216  limccnpcntop  15217  limccoap  15220  dvcoapbr  15249  eflt  15317  sin0pilem2  15324  pilem3  15325  perfectlem2  15542  lgsval2lem  15557  lgsdirnn0  15594  lgsdinn0  15595  2sqlem10  15672  2omap  16067  subctctexmid  16072  pw1nct  16075  nnsf  16077  nninfalllem1  16080  nninfsellemeqinf  16088  isomninnlem  16104  trilpolemlt1  16115  trirec0  16118  apdiff  16122  iswomninnlem  16123  ismkvnnlem  16126  redcwlpolemeq1  16128  redc0  16131  reap0  16132  cndcap  16133  dceqnconst  16134  dcapnconst  16135  nconstwlpolem0  16137  nconstwlpolem  16139  neap0mkv  16143  ltlenmkv  16144