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  6231  caofref  6259  caofinvl  6260  caofdig  6268  oprssdmm  6333  tfrlem1  6473  tfrlem5  6479  tfr1onlemsucfn  6505  tfr1onlemsucaccv  6506  tfr1onlembxssdm  6508  tfr1onlembfn  6509  tfr1onlemaccex  6513  tfr1onlemres  6514  tfrcllemsucfn  6518  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllembfn  6522  tfrcllemaccex  6526  tfrcllemres  6527  tfrcl  6529  rdgon  6551  frecabcl  6564  pw2f1odclem  7019  elssdc  7093  undifdcss  7114  ctssdclemn0  7308  ctssdc  7311  nninfninc  7321  nnnninfeq  7326  nnnninfeq2  7327  enomnilem  7336  fodju0  7345  fodjuomnilemres  7346  ismkvnex  7353  fodjumkvlemres  7357  enmkvlem  7359  enwomnilem  7367  nninfdcinf  7369  nninfwlporlem  7371  nninfwlpoimlemdc  7375  nninfinfwlpolem  7376  exmidaclem  7422  exmidontriimlem4  7438  netap  7472  exmidapne  7478  cc2lem  7484  cc3  7486  prltlu  7706  cauappcvgprlemm  7864  caucvgprlemm  7887  caucvgprprlemml  7913  suplocexprlemmu  7937  suplocexprlemdisj  7939  suplocexprlemloc  7940  suplocexprlemub  7942  caucvgsrlemgt1  8014  caucvgsr  8021  suplocsrlemb  8025  suplocsrlempr  8026  suplocsrlem  8027  axcaucvglemcau  8117  axcaucvglemres  8118  axpre-suploclemres  8120  irrmulap  9881  suprzubdc  10495  nninfdcex  10496  zsupssdc  10497  exbtwnzlemstep  10506  apbtwnz  10533  frecuzrdgsuc  10675  frecuzrdgg  10677  frecuzrdgsuctlem  10684  uzsinds  10705  iseqovex  10719  seq3val  10721  seqvalcd  10722  seq3-1  10723  seqf  10725  seq3p1  10726  seqovcd  10728  seqp1cd  10731  seq3clss  10732  seq3fveq2  10736  seqfveq2g  10738  seqfveqg  10739  seq3fveq  10740  seq3feq  10741  seq3shft2  10742  seqshft2g  10743  monoord  10746  monoord2  10747  ser3mono  10748  seq3split  10749  seqsplitg  10750  seq3caopr3  10752  seqcaopr3g  10753  iseqf1olemkle  10758  iseqf1olemklt  10759  iseqf1olemjpcl  10769  iseqf1olemqpcl  10770  iseqf1olemfvp  10771  seq3f1olemqsumkj  10772  seq3f1olemqsum  10774  seq3f1oleml  10777  seq3f1o  10778  seqf1og  10782  seq3id3  10785  seq3id  10786  seq3id2  10787  seq3homo  10788  seq3z  10789  seqhomog  10791  seqfeq4g  10792  ser3ge0  10797  nn0ltexp2  10970  zfz1isolemiso  11102  wrdind  11302  seq3shft  11398  cvg1nlemcau  11544  cvg1nlemres  11545  recvguniq  11555  resqrexlemgt0  11580  resqrexlemoverl  11581  resqrexlemglsq  11582  climi  11847  climcn1  11868  serf0  11912  fsum3cvg  11938  summodclem2  11942  summodc  11943  fsum3  11947  isumz  11949  fsumf1o  11950  isumss  11951  fisumss  11952  isumss2  11953  fsum3cvg2  11954  fsum3cvg3  11956  fsum3ser  11957  fsumsplit  11967  fsumm1  11976  fsum1p  11978  fisumcom2  11998  fsumge1  12021  telfsumo  12026  telfsumo2  12027  fsumparts  12030  isumshft  12050  isum1p  12052  isumnn0nn  12053  isumrpcl  12054  cvgratnnlemnexp  12084  cvgratnnlemmn  12085  cvgratnnlemseq  12086  cvgratnnlemabsle  12087  cvgratnnlemfm  12089  cvgratnnlemrate  12090  cvgratnn  12091  cvgratz  12092  mertenslemi1  12095  mertenslem2  12096  mertensabs  12097  fproddccvg  12132  prodmodclem2a  12136  prodmodc  12138  zproddc  12139  fprodseq  12143  prod1dc  12146  fprodf1o  12148  prodssdc  12149  fprodssdc  12150  fprodm1  12158  fprod1p  12159  fprodcom2fi  12186  sinltxirr  12321  bezoutlemmain  12568  bezoutlemex  12571  bezoutlemzz  12572  bezoutlemmo  12576  bezoutlemle  12578  bezoutlemsup  12579  nnmindc  12604  nnminle  12605  uzwodc  12607  nninfctlemfo  12610  prmind2  12691  isprm5lem  12712  isprm5  12713  pcmpt2  12916  prmpwdvds  12927  ennnfonelemk  13020  ennnfonelemex  13034  ennnfonelemnn0  13042  ctinfomlemom  13047  ctiunctlemudc  13057  ssnnctlemct  13066  nninfdclemcl  13068  nninfdclemp1  13070  nninfdc  13073  prdsbasprj  13364  lidrideqd  13463  grpinvalem  13467  grpinva  13468  grpidd2  13623  mulgsubcl  13722  issubg4m  13779  ghmf1  13859  gsumfzmhm2  13930  lringuplu  14209  mplsubgfilemcl  14712  icnpimaex  14934  lmcvg  14940  lmff  14972  cnmpt11  15006  cnmpt21  15014  comet  15222  dedekindeulemuub  15340  dedekindeulemloc  15342  dedekindeulemlu  15344  dedekindeulemeu  15345  suplociccreex  15347  suplociccex  15348  dedekindicclemuub  15349  dedekindicclemloc  15351  dedekindicclemlu  15353  dedekindicclemeu  15354  dedekindicc  15356  ivthinclemlopn  15359  ivthinclemlr  15360  ivthinclemuopn  15361  ivthinclemur  15362  ivthinclemdisj  15363  ivthinclemloc  15364  ivthinc  15366  ivthdec  15367  ivthreinc  15368  dich0  15375  limcimolemlt  15387  limcimo  15388  cnplimclemr  15392  cnlimci  15396  cnmptlimc  15397  limccnpcntop  15398  limccoap  15401  dvcoapbr  15430  eflt  15498  sin0pilem2  15505  pilem3  15506  perfectlem2  15723  lgsval2lem  15738  lgsdirnn0  15775  lgsdinn0  15776  2sqlem10  15853  2omap  16594  subctctexmid  16601  pw1nct  16604  nnsf  16607  nninfalllem1  16610  nninfsellemeqinf  16618  isomninnlem  16634  trilpolemlt1  16645  trirec0  16648  apdiff  16652  iswomninnlem  16653  ismkvnnlem  16656  redcwlpolemeq1  16658  redc0  16661  reap0  16662  cndcap  16663  dceqnconst  16664  dcapnconst  16665  nconstwlpolem0  16667  nconstwlpolem  16669  neap0mkv  16673  ltlenmkv  16674