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  7319  ctssdclemn0  7451  ctssdc  7454  nninfninc  7464  nnnninfeq  7469  nnnninfeq2  7470  enomnilem  7479  fodju0  7488  fodjuomnilemres  7489  ismkvnex  7496  fodjumkvlemres  7500  enmkvlem  7502  enwomnilem  7510  nninfdcinf  7512  nninfwlporlem  7514  nninfwlpoimlemdc  7518  nninfinfwlpolem  7519  exmidaclem  7565  exmidontriimlem4  7581  papirr  7612  papsym  7613  papcotr  7614  netap  7621  exmidapne  7627  cc2lem  7633  cc3  7635  prltlu  7855  cauappcvgprlemm  8013  caucvgprlemm  8036  caucvgprprlemml  8062  suplocexprlemmu  8086  suplocexprlemdisj  8088  suplocexprlemloc  8089  suplocexprlemub  8091  caucvgsrlemgt1  8163  caucvgsr  8170  suplocsrlemb  8174  suplocsrlempr  8175  suplocsrlem  8176  axcaucvglemcau  8266  axcaucvglemres  8267  axpre-suploclemres  8269  indfdc  9301  irraddap  10057  irrmulap  10059  suprzubdc  10682  nninfdcex  10683  zsupssdc  10684  exbtwnzlemstep  10693  apbtwnz  10720  frecuzrdgsuc  10865  frecuzrdgg  10867  frecuzrdgsuctlem  10874  uzsinds  10895  iseqovex  10909  seq3val  10911  seqvalcd  10912  seq3-1  10913  seqf  10915  seq3p1  10916  seqovcd  10918  seqp1cd  10921  seq3clss  10922  seq3fveq2  10926  seqfveq2g  10928  seqfveqg  10929  seq3fveq  10930  seq3feq  10931  seq3shft2  10932  seqshft2g  10933  monoord  10936  monoord2  10937  ser3mono  10938  seq3split  10939  seqsplitg  10940  seq3caopr3  10942  seqcaopr3g  10943  iseqf1olemkle  10948  iseqf1olemklt  10949  iseqf1olemjpcl  10959  iseqf1olemqpcl  10960  iseqf1olemfvp  10961  seq3f1olemqsumkj  10962  seq3f1olemqsum  10964  seq3f1oleml  10967  seq3f1o  10968  seqf1og  10972  seq3id3  10975  seq3id  10976  seq3id2  10977  seq3homo  10978  seq3z  10979  seqhomog  10981  seqfeq4g  10982  ser3ge0  10987  nn0ltexp2  11162  hashfibclem  11297  zfz1isolemiso  11306  wrdind  11509  seq3shft  11618  cvg1nlemcau  11765  cvg1nlemres  11766  recvguniq  11776  resqrexlemgt0  11801  resqrexlemoverl  11802  resqrexlemglsq  11803  climi  12071  climcn1  12092  serf0  12136  fsum3cvg  12163  summodclem2  12167  summodc  12168  fsum3  12172  isumz  12174  fsumf1o  12175  isumss  12176  fisumss  12177  isumss2  12178  fsum3cvg2  12179  fsum3cvg3  12181  fsum3ser  12182  fsumsplit  12192  fsumm1  12201  fsum1p  12203  fisumcom2  12223  fsumge1  12246  telfsumo  12251  telfsumo2  12252  fsumparts  12255  isumshft  12275  isum1p  12277  isumnn0nn  12278  isumrpcl  12279  cvgratnnlemnexp  12309  cvgratnnlemmn  12310  cvgratnnlemseq  12311  cvgratnnlemabsle  12312  cvgratnnlemfm  12314  cvgratnnlemrate  12315  cvgratnn  12316  cvgratz  12317  mertenslemi1  12320  mertenslem2  12321  mertensabs  12322  fproddccvg  12357  prodmodclem2a  12361  prodmodc  12363  zproddc  12364  fprodseq  12368  prod1dc  12371  fprodf1o  12373  prodssdc  12374  fprodssdc  12375  fprodm1  12383  fprod1p  12384  fprodcom2fi  12411  sinltxirr  12546  bezoutlemmain  12793  bezoutlemex  12796  bezoutlemzz  12797  bezoutlemmo  12801  bezoutlemle  12803  bezoutlemsup  12804  nnmindc  12829  nnminle  12830  uzwodc  12832  nninfctlemfo  12835  prmind2  12916  isprm5lem  12938  isprm5  12939  pcmpt2  13145  prmpwdvds  13156  ennnfonelemk  13342  ennnfonelemex  13356  ennnfonelemnn0  13364  ctinfomlemom  13369  ctiunctlemudc  13379  ssnnctlemct  13388  nninfdclemcl  13390  nninfdclemp1  13392  nninfdc  13395  lidrideqd  13752  grpinvalem  13756  grpinva  13757  grpidd2  13897  mulgsubcl  13990  issubg4m  14047  ghmf1  14127  gzsummhm2  14197  gsummhm2fi  14216  prdsbasprj  14233  lringuplu  14554  psrbaglefifi  15114  mplsubgfilemcl  15142  icnpimaex  15364  lmcvg  15370  lmff  15402  cnmpt11  15436  cnmpt21  15444  comet  15652  dedekindeulemuub  15770  dedekindeulemloc  15772  dedekindeulemlu  15774  dedekindeulemeu  15775  suplociccreex  15777  suplociccex  15778  dedekindicclemuub  15779  dedekindicclemloc  15781  dedekindicclemlu  15783  dedekindicclemeu  15784  dedekindicc  15786  ivthinclemlopn  15789  ivthinclemlr  15790  ivthinclemuopn  15791  ivthinclemur  15792  ivthinclemdisj  15793  ivthinclemloc  15794  ivthinc  15796  ivthdec  15797  ivthreinc  15798  dich0  15805  limcimolemlt  15817  limcimo  15818  cnplimclemr  15822  cnlimci  15826  cnmptlimc  15827  limccnpcntop  15828  limccoap  15831  dvcoapbr  15860  eflt  15928  sin0pilem2  15936  pilem3  15937  chtqub  16218  perfectlem2  16222  lgsval2lem  16251  lgsdirnn0  16288  lgsdinn0  16289  2sqlem10  16366  eupth2lem3fi  16839  subctctexmid  17152  pw1nct  17155  exmidnotnotr  17158  exmidcon  17159  exmidpeirce  17160  nnsf  17170  nninfalllem1  17173  nninfsellemeqinf  17181  isomninnlem  17201  trilpolemlt1  17212  trirec0  17215  apdiff  17219  iswomninnlem  17221  ismkvnnlem  17224  redcwlpolemeq1  17226  redc0  17229  reap0  17230  cndcap  17231  dceqnconst  17232  dcapnconst  17233  nconstwlpolem0  17235  nconstwlpolem  17237  neap0mkv  17241  ltlenmkv  17242