Theorem rspcdva 2915

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397   ∈ wcel 2202  ∀wral 2510

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-v 2804

This theorem is referenced by:  frirrg  4447  wetriext  4675  tfisi  4685  omsinds  4720  suppssov1  6232  caofref  6260  caofinvl  6261  caofdig  6269  oprssdmm  6334  tfrlem1  6474  tfrlem5  6480  tfr1onlemsucfn  6506  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfr1onlemaccex  6514  tfr1onlemres  6515  tfrcllemsucfn  6519  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllembfn  6523  tfrcllemaccex  6527  tfrcllemres  6528  tfrcl  6530  rdgon  6552  frecabcl  6565  pw2f1odclem  7020  elssdc  7094  undifdcss  7115  ctssdclemn0  7309  ctssdc  7312  nninfninc  7322  nnnninfeq  7327  nnnninfeq2  7328  enomnilem  7337  fodju0  7346  fodjuomnilemres  7347  ismkvnex  7354  fodjumkvlemres  7358  enmkvlem  7360  enwomnilem  7368  nninfdcinf  7370  nninfwlporlem  7372  nninfwlpoimlemdc  7376  nninfinfwlpolem  7377  exmidaclem  7423  exmidontriimlem4  7439  netap  7473  exmidapne  7479  cc2lem  7485  cc3  7487  prltlu  7707  cauappcvgprlemm  7865  caucvgprlemm  7888  caucvgprprlemml  7914  suplocexprlemmu  7938  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemub  7943  caucvgsrlemgt1  8015  caucvgsr  8022  suplocsrlemb  8026  suplocsrlempr  8027  suplocsrlem  8028  axcaucvglemcau  8118  axcaucvglemres  8119  axpre-suploclemres  8121  irrmulap  9882  suprzubdc  10497  nninfdcex  10498  zsupssdc  10499  exbtwnzlemstep  10508  apbtwnz  10535  frecuzrdgsuc  10677  frecuzrdgg  10679  frecuzrdgsuctlem  10686  uzsinds  10707  iseqovex  10721  seq3val  10723  seqvalcd  10724  seq3-1  10725  seqf  10727  seq3p1  10728  seqovcd  10730  seqp1cd  10733  seq3clss  10734  seq3fveq2  10738  seqfveq2g  10740  seqfveqg  10741  seq3fveq  10742  seq3feq  10743  seq3shft2  10744  seqshft2g  10745  monoord  10748  monoord2  10749  ser3mono  10750  seq3split  10751  seqsplitg  10752  seq3caopr3  10754  seqcaopr3g  10755  iseqf1olemkle  10760  iseqf1olemklt  10761  iseqf1olemjpcl  10771  iseqf1olemqpcl  10772  iseqf1olemfvp  10773  seq3f1olemqsumkj  10774  seq3f1olemqsum  10776  seq3f1oleml  10779  seq3f1o  10780  seqf1og  10784  seq3id3  10787  seq3id  10788  seq3id2  10789  seq3homo  10790  seq3z  10791  seqhomog  10793  seqfeq4g  10794  ser3ge0  10799  nn0ltexp2  10972  zfz1isolemiso  11104  wrdind  11307  seq3shft  11403  cvg1nlemcau  11549  cvg1nlemres  11550  recvguniq  11560  resqrexlemgt0  11585  resqrexlemoverl  11586  resqrexlemglsq  11587  climi  11852  climcn1  11873  serf0  11917  fsum3cvg  11944  summodclem2  11948  summodc  11949  fsum3  11953  isumz  11955  fsumf1o  11956  isumss  11957  fisumss  11958  isumss2  11959  fsum3cvg2  11960  fsum3cvg3  11962  fsum3ser  11963  fsumsplit  11973  fsumm1  11982  fsum1p  11984  fisumcom2  12004  fsumge1  12027  telfsumo  12032  telfsumo2  12033  fsumparts  12036  isumshft  12056  isum1p  12058  isumnn0nn  12059  isumrpcl  12060  cvgratnnlemnexp  12090  cvgratnnlemmn  12091  cvgratnnlemseq  12092  cvgratnnlemabsle  12093  cvgratnnlemfm  12095  cvgratnnlemrate  12096  cvgratnn  12097  cvgratz  12098  mertenslemi1  12101  mertenslem2  12102  mertensabs  12103  fproddccvg  12138  prodmodclem2a  12142  prodmodc  12144  zproddc  12145  fprodseq  12149  prod1dc  12152  fprodf1o  12154  prodssdc  12155  fprodssdc  12156  fprodm1  12164  fprod1p  12165  fprodcom2fi  12192  sinltxirr  12327  bezoutlemmain  12574  bezoutlemex  12577  bezoutlemzz  12578  bezoutlemmo  12582  bezoutlemle  12584  bezoutlemsup  12585  nnmindc  12610  nnminle  12611  uzwodc  12613  nninfctlemfo  12616  prmind2  12697  isprm5lem  12718  isprm5  12719  pcmpt2  12922  prmpwdvds  12933  ennnfonelemk  13026  ennnfonelemex  13040  ennnfonelemnn0  13048  ctinfomlemom  13053  ctiunctlemudc  13063  ssnnctlemct  13072  nninfdclemcl  13074  nninfdclemp1  13076  nninfdc  13079  prdsbasprj  13370  lidrideqd  13469  grpinvalem  13473  grpinva  13474  grpidd2  13629  mulgsubcl  13728  issubg4m  13785  ghmf1  13865  gsumfzmhm2  13936  lringuplu  14216  mplsubgfilemcl  14719  icnpimaex  14941  lmcvg  14947  lmff  14979  cnmpt11  15013  cnmpt21  15021  comet  15229  dedekindeulemuub  15347  dedekindeulemloc  15349  dedekindeulemlu  15351  dedekindeulemeu  15352  suplociccreex  15354  suplociccex  15355  dedekindicclemuub  15356  dedekindicclemloc  15358  dedekindicclemlu  15360  dedekindicclemeu  15361  dedekindicc  15363  ivthinclemlopn  15366  ivthinclemlr  15367  ivthinclemuopn  15368  ivthinclemur  15369  ivthinclemdisj  15370  ivthinclemloc  15371  ivthinc  15373  ivthdec  15374  ivthreinc  15375  dich0  15382  limcimolemlt  15394  limcimo  15395  cnplimclemr  15399  cnlimci  15403  cnmptlimc  15404  limccnpcntop  15405  limccoap  15408  dvcoapbr  15437  eflt  15505  sin0pilem2  15512  pilem3  15513  perfectlem2  15730  lgsval2lem  15745  lgsdirnn0  15782  lgsdinn0  15783  2sqlem10  15860  eupth2lem3fi  16333  2omap  16620  subctctexmid  16627  pw1nct  16630  nnsf  16633  nninfalllem1  16636  nninfsellemeqinf  16644  isomninnlem  16660  trilpolemlt1  16671  trirec0  16674  apdiff  16678  iswomninnlem  16680  ismkvnnlem  16683  redcwlpolemeq1  16685  redc0  16688  reap0  16689  cndcap  16690  dceqnconst  16691  dcapnconst  16692  nconstwlpolem0  16694  nconstwlpolem  16696  neap0mkv  16700  ltlenmkv  16701