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  9300  irraddap  10056  irrmulap  10058  suprzubdc  10681  nninfdcex  10682  zsupssdc  10683  exbtwnzlemstep  10692  apbtwnz  10719  frecuzrdgsuc  10864  frecuzrdgg  10866  frecuzrdgsuctlem  10873  uzsinds  10894  iseqovex  10908  seq3val  10910  seqvalcd  10911  seq3-1  10912  seqf  10914  seq3p1  10915  seqovcd  10917  seqp1cd  10920  seq3clss  10921  seq3fveq2  10925  seqfveq2g  10927  seqfveqg  10928  seq3fveq  10929  seq3feq  10930  seq3shft2  10931  seqshft2g  10932  monoord  10935  monoord2  10936  ser3mono  10937  seq3split  10938  seqsplitg  10939  seq3caopr3  10941  seqcaopr3g  10942  iseqf1olemkle  10947  iseqf1olemklt  10948  iseqf1olemjpcl  10958  iseqf1olemqpcl  10959  iseqf1olemfvp  10960  seq3f1olemqsumkj  10961  seq3f1olemqsum  10963  seq3f1oleml  10966  seq3f1o  10967  seqf1og  10971  seq3id3  10974  seq3id  10975  seq3id2  10976  seq3homo  10977  seq3z  10978  seqhomog  10980  seqfeq4g  10981  ser3ge0  10986  nn0ltexp2  11161  hashfibclem  11296  zfz1isolemiso  11305  wrdind  11508  seq3shft  11617  cvg1nlemcau  11764  cvg1nlemres  11765  recvguniq  11775  resqrexlemgt0  11800  resqrexlemoverl  11801  resqrexlemglsq  11802  climi  12069  climcn1  12090  serf0  12134  fsum3cvg  12161  summodclem2  12165  summodc  12166  fsum3  12170  isumz  12172  fsumf1o  12173  isumss  12174  fisumss  12175  isumss2  12176  fsum3cvg2  12177  fsum3cvg3  12179  fsum3ser  12180  fsumsplit  12190  fsumm1  12199  fsum1p  12201  fisumcom2  12221  fsumge1  12244  telfsumo  12249  telfsumo2  12250  fsumparts  12253  isumshft  12273  isum1p  12275  isumnn0nn  12276  isumrpcl  12277  cvgratnnlemnexp  12307  cvgratnnlemmn  12308  cvgratnnlemseq  12309  cvgratnnlemabsle  12310  cvgratnnlemfm  12312  cvgratnnlemrate  12313  cvgratnn  12314  cvgratz  12315  mertenslemi1  12318  mertenslem2  12319  mertensabs  12320  fproddccvg  12355  prodmodclem2a  12359  prodmodc  12361  zproddc  12362  fprodseq  12366  prod1dc  12369  fprodf1o  12371  prodssdc  12372  fprodssdc  12373  fprodm1  12381  fprod1p  12382  fprodcom2fi  12409  sinltxirr  12544  bezoutlemmain  12791  bezoutlemex  12794  bezoutlemzz  12795  bezoutlemmo  12799  bezoutlemle  12801  bezoutlemsup  12802  nnmindc  12827  nnminle  12828  uzwodc  12830  nninfctlemfo  12833  prmind2  12914  isprm5lem  12936  isprm5  12937  pcmpt2  13143  prmpwdvds  13154  ennnfonelemk  13340  ennnfonelemex  13354  ennnfonelemnn0  13362  ctinfomlemom  13367  ctiunctlemudc  13377  ssnnctlemct  13386  nninfdclemcl  13388  nninfdclemp1  13390  nninfdc  13393  lidrideqd  13750  grpinvalem  13754  grpinva  13755  grpidd2  13895  mulgsubcl  13988  issubg4m  14045  ghmf1  14125  gzsummhm2  14195  gsummhm2fi  14214  prdsbasprj  14231  lringuplu  14552  mplsubgfilemcl  15139  icnpimaex  15361  lmcvg  15367  lmff  15399  cnmpt11  15433  cnmpt21  15441  comet  15649  dedekindeulemuub  15767  dedekindeulemloc  15769  dedekindeulemlu  15771  dedekindeulemeu  15772  suplociccreex  15774  suplociccex  15775  dedekindicclemuub  15776  dedekindicclemloc  15778  dedekindicclemlu  15780  dedekindicclemeu  15781  dedekindicc  15783  ivthinclemlopn  15786  ivthinclemlr  15787  ivthinclemuopn  15788  ivthinclemur  15789  ivthinclemdisj  15790  ivthinclemloc  15791  ivthinc  15793  ivthdec  15794  ivthreinc  15795  dich0  15802  limcimolemlt  15814  limcimo  15815  cnplimclemr  15819  cnlimci  15823  cnmptlimc  15824  limccnpcntop  15825  limccoap  15828  dvcoapbr  15857  eflt  15925  sin0pilem2  15933  pilem3  15934  perfectlem2  16198  lgsval2lem  16227  lgsdirnn0  16264  lgsdinn0  16265  2sqlem10  16342  eupth2lem3fi  16815  subctctexmid  17128  pw1nct  17131  exmidnotnotr  17134  exmidcon  17135  exmidpeirce  17136  nnsf  17146  nninfalllem1  17149  nninfsellemeqinf  17157  isomninnlem  17177  trilpolemlt1  17188  trirec0  17191  apdiff  17195  iswomninnlem  17197  ismkvnnlem  17200  redcwlpolemeq1  17202  redc0  17205  reap0  17206  cndcap  17207  dceqnconst  17208  dcapnconst  17209  nconstwlpolem0  17211  nconstwlpolem  17213  neap0mkv  17217  ltlenmkv  17218