Theorem rspcdva 2913

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395   ∈ wcel 2200  ∀wral 2508

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2802

This theorem is referenced by:  frirrg  4445  wetriext  4673  tfisi  4683  omsinds  4718  suppssov1  6227  caofref  6255  caofinvl  6256  caofdig  6264  oprssdmm  6329  tfrlem1  6469  tfrlem5  6475  tfr1onlemsucfn  6501  tfr1onlemsucaccv  6502  tfr1onlembxssdm  6504  tfr1onlembfn  6505  tfr1onlemaccex  6509  tfr1onlemres  6510  tfrcllemsucfn  6514  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllembfn  6518  tfrcllemaccex  6522  tfrcllemres  6523  tfrcl  6525  rdgon  6547  frecabcl  6560  pw2f1odclem  7015  elssdc  7087  undifdcss  7108  ctssdclemn0  7300  ctssdc  7303  nninfninc  7313  nnnninfeq  7318  nnnninfeq2  7319  enomnilem  7328  fodju0  7337  fodjuomnilemres  7338  ismkvnex  7345  fodjumkvlemres  7349  enmkvlem  7351  enwomnilem  7359  nninfdcinf  7361  nninfwlporlem  7363  nninfwlpoimlemdc  7367  nninfinfwlpolem  7368  exmidaclem  7413  exmidontriimlem4  7429  netap  7463  exmidapne  7469  cc2lem  7475  cc3  7477  prltlu  7697  cauappcvgprlemm  7855  caucvgprlemm  7878  caucvgprprlemml  7904  suplocexprlemmu  7928  suplocexprlemdisj  7930  suplocexprlemloc  7931  suplocexprlemub  7933  caucvgsrlemgt1  8005  caucvgsr  8012  suplocsrlemb  8016  suplocsrlempr  8017  suplocsrlem  8018  axcaucvglemcau  8108  axcaucvglemres  8109  axpre-suploclemres  8111  irrmulap  9872  suprzubdc  10486  nninfdcex  10487  zsupssdc  10488  exbtwnzlemstep  10497  apbtwnz  10524  frecuzrdgsuc  10666  frecuzrdgg  10668  frecuzrdgsuctlem  10675  uzsinds  10696  iseqovex  10710  seq3val  10712  seqvalcd  10713  seq3-1  10714  seqf  10716  seq3p1  10717  seqovcd  10719  seqp1cd  10722  seq3clss  10723  seq3fveq2  10727  seqfveq2g  10729  seqfveqg  10730  seq3fveq  10731  seq3feq  10732  seq3shft2  10733  seqshft2g  10734  monoord  10737  monoord2  10738  ser3mono  10739  seq3split  10740  seqsplitg  10741  seq3caopr3  10743  seqcaopr3g  10744  iseqf1olemkle  10749  iseqf1olemklt  10750  iseqf1olemjpcl  10760  iseqf1olemqpcl  10761  iseqf1olemfvp  10762  seq3f1olemqsumkj  10763  seq3f1olemqsum  10765  seq3f1oleml  10768  seq3f1o  10769  seqf1og  10773  seq3id3  10776  seq3id  10777  seq3id2  10778  seq3homo  10779  seq3z  10780  seqhomog  10782  seqfeq4g  10783  ser3ge0  10788  nn0ltexp2  10961  zfz1isolemiso  11093  wrdind  11293  seq3shft  11389  cvg1nlemcau  11535  cvg1nlemres  11536  recvguniq  11546  resqrexlemgt0  11571  resqrexlemoverl  11572  resqrexlemglsq  11573  climi  11838  climcn1  11859  serf0  11903  fsum3cvg  11929  summodclem2  11933  summodc  11934  fsum3  11938  isumz  11940  fsumf1o  11941  isumss  11942  fisumss  11943  isumss2  11944  fsum3cvg2  11945  fsum3cvg3  11947  fsum3ser  11948  fsumsplit  11958  fsumm1  11967  fsum1p  11969  fisumcom2  11989  fsumge1  12012  telfsumo  12017  telfsumo2  12018  fsumparts  12021  isumshft  12041  isum1p  12043  isumnn0nn  12044  isumrpcl  12045  cvgratnnlemnexp  12075  cvgratnnlemmn  12076  cvgratnnlemseq  12077  cvgratnnlemabsle  12078  cvgratnnlemfm  12080  cvgratnnlemrate  12081  cvgratnn  12082  cvgratz  12083  mertenslemi1  12086  mertenslem2  12087  mertensabs  12088  fproddccvg  12123  prodmodclem2a  12127  prodmodc  12129  zproddc  12130  fprodseq  12134  prod1dc  12137  fprodf1o  12139  prodssdc  12140  fprodssdc  12141  fprodm1  12149  fprod1p  12150  fprodcom2fi  12177  sinltxirr  12312  bezoutlemmain  12559  bezoutlemex  12562  bezoutlemzz  12563  bezoutlemmo  12567  bezoutlemle  12569  bezoutlemsup  12570  nnmindc  12595  nnminle  12596  uzwodc  12598  nninfctlemfo  12601  prmind2  12682  isprm5lem  12703  isprm5  12704  pcmpt2  12907  prmpwdvds  12918  ennnfonelemk  13011  ennnfonelemex  13025  ennnfonelemnn0  13033  ctinfomlemom  13038  ctiunctlemudc  13048  ssnnctlemct  13057  nninfdclemcl  13059  nninfdclemp1  13061  nninfdc  13064  prdsbasprj  13355  lidrideqd  13454  grpinvalem  13458  grpinva  13459  grpidd2  13614  mulgsubcl  13713  issubg4m  13770  ghmf1  13850  gsumfzmhm2  13921  lringuplu  14200  mplsubgfilemcl  14703  icnpimaex  14925  lmcvg  14931  lmff  14963  cnmpt11  14997  cnmpt21  15005  comet  15213  dedekindeulemuub  15331  dedekindeulemloc  15333  dedekindeulemlu  15335  dedekindeulemeu  15336  suplociccreex  15338  suplociccex  15339  dedekindicclemuub  15340  dedekindicclemloc  15342  dedekindicclemlu  15344  dedekindicclemeu  15345  dedekindicc  15347  ivthinclemlopn  15350  ivthinclemlr  15351  ivthinclemuopn  15352  ivthinclemur  15353  ivthinclemdisj  15354  ivthinclemloc  15355  ivthinc  15357  ivthdec  15358  ivthreinc  15359  dich0  15366  limcimolemlt  15378  limcimo  15379  cnplimclemr  15383  cnlimci  15387  cnmptlimc  15388  limccnpcntop  15389  limccoap  15392  dvcoapbr  15421  eflt  15489  sin0pilem2  15496  pilem3  15497  perfectlem2  15714  lgsval2lem  15729  lgsdirnn0  15766  lgsdinn0  15767  2sqlem10  15844  2omap  16530  subctctexmid  16537  pw1nct  16540  nnsf  16543  nninfalllem1  16546  nninfsellemeqinf  16554  isomninnlem  16570  trilpolemlt1  16581  trirec0  16584  apdiff  16588  iswomninnlem  16589  ismkvnnlem  16592  redcwlpolemeq1  16594  redc0  16597  reap0  16598  cndcap  16599  dceqnconst  16600  dcapnconst  16601  nconstwlpolem0  16603  nconstwlpolem  16605  neap0mkv  16609  ltlenmkv  16610