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 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1402   ∈ wcel 2209  ∀wral 2528

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 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 theorem 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 referenced by:  frirrg  4490  wetriext  4719  tfisi  4729  omsinds  4764  suppssov1  6289  caofref  6317  caofinvl  6318  caofdig  6326  oprssdmm  6395  suppssdc  6490  suppssrst  6491  suppssrgst  6492  suppofss1dcl  6494  suppofss2dcl  6495  tfrlem1  6569  tfrlem5  6575  tfr1onlemsucfn  6601  tfr1onlemsucaccv  6602  tfr1onlembxssdm  6604  tfr1onlembfn  6605  tfr1onlemaccex  6609  tfr1onlemres  6610  tfrcllemsucfn  6614  tfrcllemsucaccv  6615  tfrcllembxssdm  6617  tfrcllembfn  6618  tfrcllemaccex  6622  tfrcllemres  6623  tfrcl  6625  rdgon  6647  frecabcl  6660  pw2f1odclem  7124  elssdc  7199  undifdcss  7220  2omap  7308  ctssdclemn0  7440  ctssdc  7443  nninfninc  7453  nnnninfeq  7458  nnnninfeq2  7459  enomnilem  7468  fodju0  7477  fodjuomnilemres  7478  ismkvnex  7485  fodjumkvlemres  7489  enmkvlem  7491  enwomnilem  7499  nninfdcinf  7501  nninfwlporlem  7503  nninfwlpoimlemdc  7507  nninfinfwlpolem  7508  exmidaclem  7554  exmidontriimlem4  7570  papirr  7601  papsym  7602  papcotr  7603  netap  7610  exmidapne  7616  cc2lem  7622  cc3  7624  prltlu  7844  cauappcvgprlemm  8002  caucvgprlemm  8025  caucvgprprlemml  8051  suplocexprlemmu  8075  suplocexprlemdisj  8077  suplocexprlemloc  8078  suplocexprlemub  8080  caucvgsrlemgt1  8152  caucvgsr  8159  suplocsrlemb  8163  suplocsrlempr  8164  suplocsrlem  8165  axcaucvglemcau  8255  axcaucvglemres  8256  axpre-suploclemres  8258  irrmulap  10027  suprzubdc  10649  nninfdcex  10650  zsupssdc  10651  exbtwnzlemstep  10660  apbtwnz  10687  frecuzrdgsuc  10829  frecuzrdgg  10831  frecuzrdgsuctlem  10838  uzsinds  10859  iseqovex  10873  seq3val  10875  seqvalcd  10876  seq3-1  10877  seqf  10879  seq3p1  10880  seqovcd  10882  seqp1cd  10885  seq3clss  10886  seq3fveq2  10890  seqfveq2g  10892  seqfveqg  10893  seq3fveq  10894  seq3feq  10895  seq3shft2  10896  seqshft2g  10897  monoord  10900  monoord2  10901  ser3mono  10902  seq3split  10903  seqsplitg  10904  seq3caopr3  10906  seqcaopr3g  10907  iseqf1olemkle  10912  iseqf1olemklt  10913  iseqf1olemjpcl  10923  iseqf1olemqpcl  10924  iseqf1olemfvp  10925  seq3f1olemqsumkj  10926  seq3f1olemqsum  10928  seq3f1oleml  10931  seq3f1o  10932  seqf1og  10936  seq3id3  10939  seq3id  10940  seq3id2  10941  seq3homo  10942  seq3z  10943  seqhomog  10945  seqfeq4g  10946  ser3ge0  10951  nn0ltexp2  11125  hashfibclem  11260  zfz1isolemiso  11269  wrdind  11472  seq3shft  11581  cvg1nlemcau  11728  cvg1nlemres  11729  recvguniq  11739  resqrexlemgt0  11764  resqrexlemoverl  11765  resqrexlemglsq  11766  climi  12031  climcn1  12052  serf0  12096  fsum3cvg  12123  summodclem2  12127  summodc  12128  fsum3  12132  isumz  12134  fsumf1o  12135  isumss  12136  fisumss  12137  isumss2  12138  fsum3cvg2  12139  fsum3cvg3  12141  fsum3ser  12142  fsumsplit  12152  fsumm1  12161  fsum1p  12163  fisumcom2  12183  fsumge1  12206  telfsumo  12211  telfsumo2  12212  fsumparts  12215  isumshft  12235  isum1p  12237  isumnn0nn  12238  isumrpcl  12239  cvgratnnlemnexp  12269  cvgratnnlemmn  12270  cvgratnnlemseq  12271  cvgratnnlemabsle  12272  cvgratnnlemfm  12274  cvgratnnlemrate  12275  cvgratnn  12276  cvgratz  12277  mertenslemi1  12280  mertenslem2  12281  mertensabs  12282  fproddccvg  12317  prodmodclem2a  12321  prodmodc  12323  zproddc  12324  fprodseq  12328  prod1dc  12331  fprodf1o  12333  prodssdc  12334  fprodssdc  12335  fprodm1  12343  fprod1p  12344  fprodcom2fi  12371  sinltxirr  12506  bezoutlemmain  12753  bezoutlemex  12756  bezoutlemzz  12757  bezoutlemmo  12761  bezoutlemle  12763  bezoutlemsup  12764  nnmindc  12789  nnminle  12790  uzwodc  12792  nninfctlemfo  12795  prmind2  12876  isprm5lem  12897  isprm5  12898  pcmpt2  13101  prmpwdvds  13112  ennnfonelemk  13269  ennnfonelemex  13283  ennnfonelemnn0  13291  ctinfomlemom  13296  ctiunctlemudc  13306  ssnnctlemct  13315  nninfdclemcl  13317  nninfdclemp1  13319  nninfdc  13322  lidrideqd  13678  grpinvalem  13682  grpinva  13683  grpidd2  13823  mulgsubcl  13916  issubg4m  13973  ghmf1  14053  gzsummhm2  14123  gsummhm2fi  14142  prdsbasprj  14159  lringuplu  14476  mplsubgfilemcl  15013  icnpimaex  15235  lmcvg  15241  lmff  15273  cnmpt11  15307  cnmpt21  15315  comet  15523  dedekindeulemuub  15641  dedekindeulemloc  15643  dedekindeulemlu  15645  dedekindeulemeu  15646  suplociccreex  15648  suplociccex  15649  dedekindicclemuub  15650  dedekindicclemloc  15652  dedekindicclemlu  15654  dedekindicclemeu  15655  dedekindicc  15657  ivthinclemlopn  15660  ivthinclemlr  15661  ivthinclemuopn  15662  ivthinclemur  15663  ivthinclemdisj  15664  ivthinclemloc  15665  ivthinc  15667  ivthdec  15668  ivthreinc  15669  dich0  15676  limcimolemlt  15688  limcimo  15689  cnplimclemr  15693  cnlimci  15697  cnmptlimc  15698  limccnpcntop  15699  limccoap  15702  dvcoapbr  15731  eflt  15799  sin0pilem2  15806  pilem3  15807  perfectlem2  16028  lgsval2lem  16043  lgsdirnn0  16080  lgsdinn0  16081  2sqlem10  16158  eupth2lem3fi  16631  subctctexmid  16944  pw1nct  16947  exmidnotnotr  16949  exmidcon  16950  exmidpeirce  16951  nnsf  16953  nninfalllem1  16956  nninfsellemeqinf  16964  isomninnlem  16984  trilpolemlt1  16995  trirec0  16998  apdiff  17002  iswomninnlem  17004  ismkvnnlem  17007  redcwlpolemeq1  17009  redc0  17012  reap0  17013  cndcap  17014  dceqnconst  17015  dcapnconst  17016  nconstwlpolem0  17018  nconstwlpolem  17020  neap0mkv  17024  ltlenmkv  17025