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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402   ∈ wcel 2209  ∀wral 2528

This proof depends on 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 proof 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 used by:  frirrg  4495  wetriext  4724  tfisi  4734  omsinds  4769  suppssov1  6299  caofref  6327  caofinvl  6328  caofdig  6336  oprssdmm  6405  suppssdc  6500  suppssrst  6501  suppssrgst  6502  suppofss1dcl  6504  suppofss2dcl  6505  tfrlem1  6579  tfrlem5  6585  tfr1onlemsucfn  6611  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemaccex  6619  tfr1onlemres  6620  tfrcllemsucfn  6624  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemaccex  6632  tfrcllemres  6633  tfrcl  6635  rdgon  6657  frecabcl  6670  pw2f1odclem  7134  elssdc  7209  undifdcss  7230  2omap  7318  ctssdclemn0  7450  ctssdc  7453  nninfninc  7463  nnnninfeq  7468  nnnninfeq2  7469  enomnilem  7478  fodju0  7487  fodjuomnilemres  7488  ismkvnex  7495  fodjumkvlemres  7499  enmkvlem  7501  enwomnilem  7509  nninfdcinf  7511  nninfwlporlem  7513  nninfwlpoimlemdc  7517  nninfinfwlpolem  7518  exmidaclem  7564  exmidontriimlem4  7580  papirr  7611  papsym  7612  papcotr  7613  netap  7620  exmidapne  7626  cc2lem  7632  cc3  7634  prltlu  7854  cauappcvgprlemm  8012  caucvgprlemm  8035  caucvgprprlemml  8061  suplocexprlemmu  8085  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemub  8090  caucvgsrlemgt1  8162  caucvgsr  8169  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  axcaucvglemcau  8265  axcaucvglemres  8266  axpre-suploclemres  8268  indfdc  9298  irrmulap  10048  suprzubdc  10671  nninfdcex  10672  zsupssdc  10673  exbtwnzlemstep  10682  apbtwnz  10709  frecuzrdgsuc  10851  frecuzrdgg  10853  frecuzrdgsuctlem  10860  uzsinds  10881  iseqovex  10895  seq3val  10897  seqvalcd  10898  seq3-1  10899  seqf  10901  seq3p1  10902  seqovcd  10904  seqp1cd  10907  seq3clss  10908  seq3fveq2  10912  seqfveq2g  10914  seqfveqg  10915  seq3fveq  10916  seq3feq  10917  seq3shft2  10918  seqshft2g  10919  monoord  10922  monoord2  10923  ser3mono  10924  seq3split  10925  seqsplitg  10926  seq3caopr3  10928  seqcaopr3g  10929  iseqf1olemkle  10934  iseqf1olemklt  10935  iseqf1olemjpcl  10945  iseqf1olemqpcl  10946  iseqf1olemfvp  10947  seq3f1olemqsumkj  10948  seq3f1olemqsum  10950  seq3f1oleml  10953  seq3f1o  10954  seqf1og  10958  seq3id3  10961  seq3id  10962  seq3id2  10963  seq3homo  10964  seq3z  10965  seqhomog  10967  seqfeq4g  10968  ser3ge0  10973  nn0ltexp2  11147  hashfibclem  11282  zfz1isolemiso  11291  wrdind  11494  seq3shft  11603  cvg1nlemcau  11750  cvg1nlemres  11751  recvguniq  11761  resqrexlemgt0  11786  resqrexlemoverl  11787  resqrexlemglsq  11788  climi  12053  climcn1  12074  serf0  12118  fsum3cvg  12145  summodclem2  12149  summodc  12150  fsum3  12154  isumz  12156  fsumf1o  12157  isumss  12158  fisumss  12159  isumss2  12160  fsum3cvg2  12161  fsum3cvg3  12163  fsum3ser  12164  fsumsplit  12174  fsumm1  12183  fsum1p  12185  fisumcom2  12205  fsumge1  12228  telfsumo  12233  telfsumo2  12234  fsumparts  12237  isumshft  12257  isum1p  12259  isumnn0nn  12260  isumrpcl  12261  cvgratnnlemnexp  12291  cvgratnnlemmn  12292  cvgratnnlemseq  12293  cvgratnnlemabsle  12294  cvgratnnlemfm  12296  cvgratnnlemrate  12297  cvgratnn  12298  cvgratz  12299  mertenslemi1  12302  mertenslem2  12303  mertensabs  12304  fproddccvg  12339  prodmodclem2a  12343  prodmodc  12345  zproddc  12346  fprodseq  12350  prod1dc  12353  fprodf1o  12355  prodssdc  12356  fprodssdc  12357  fprodm1  12365  fprod1p  12366  fprodcom2fi  12393  sinltxirr  12528  bezoutlemmain  12775  bezoutlemex  12778  bezoutlemzz  12779  bezoutlemmo  12783  bezoutlemle  12785  bezoutlemsup  12786  nnmindc  12811  nnminle  12812  uzwodc  12814  nninfctlemfo  12817  prmind2  12898  isprm5lem  12919  isprm5  12920  pcmpt2  13123  prmpwdvds  13134  ennnfonelemk  13291  ennnfonelemex  13305  ennnfonelemnn0  13313  ctinfomlemom  13318  ctiunctlemudc  13328  ssnnctlemct  13337  nninfdclemcl  13339  nninfdclemp1  13341  nninfdc  13344  lidrideqd  13701  grpinvalem  13705  grpinva  13706  grpidd2  13846  mulgsubcl  13939  issubg4m  13996  ghmf1  14076  gzsummhm2  14146  gsummhm2fi  14165  prdsbasprj  14182  lringuplu  14503  mplsubgfilemcl  15090  icnpimaex  15312  lmcvg  15318  lmff  15350  cnmpt11  15384  cnmpt21  15392  comet  15600  dedekindeulemuub  15718  dedekindeulemloc  15720  dedekindeulemlu  15722  dedekindeulemeu  15723  suplociccreex  15725  suplociccex  15726  dedekindicclemuub  15727  dedekindicclemloc  15729  dedekindicclemlu  15731  dedekindicclemeu  15732  dedekindicc  15734  ivthinclemlopn  15737  ivthinclemlr  15738  ivthinclemuopn  15739  ivthinclemur  15740  ivthinclemdisj  15741  ivthinclemloc  15742  ivthinc  15744  ivthdec  15745  ivthreinc  15746  dich0  15753  limcimolemlt  15765  limcimo  15766  cnplimclemr  15770  cnlimci  15774  cnmptlimc  15775  limccnpcntop  15776  limccoap  15779  dvcoapbr  15808  eflt  15876  sin0pilem2  15883  pilem3  15884  perfectlem2  16114  lgsval2lem  16129  lgsdirnn0  16166  lgsdinn0  16167  2sqlem10  16244  eupth2lem3fi  16717  subctctexmid  17030  pw1nct  17033  exmidnotnotr  17036  exmidcon  17037  exmidpeirce  17038  nnsf  17048  nninfalllem1  17051  nninfsellemeqinf  17059  isomninnlem  17079  trilpolemlt1  17090  trirec0  17093  apdiff  17097  iswomninnlem  17099  ismkvnnlem  17102  redcwlpolemeq1  17104  redc0  17107  reap0  17108  cndcap  17109  dceqnconst  17110  dcapnconst  17111  nconstwlpolem0  17113  nconstwlpolem  17115  neap0mkv  17119  ltlenmkv  17120