Theorem rspcdva 2912

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 2903	. 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 2801

This theorem is referenced by:  frirrg  4440  wetriext  4668  tfisi  4678  omsinds  4713  suppssov1  6213  caofref  6241  caofinvl  6242  caofdig  6250  oprssdmm  6315  tfrlem1  6452  tfrlem5  6458  tfr1onlemsucfn  6484  tfr1onlemsucaccv  6485  tfr1onlembxssdm  6487  tfr1onlembfn  6488  tfr1onlemaccex  6492  tfr1onlemres  6493  tfrcllemsucfn  6497  tfrcllemsucaccv  6498  tfrcllembxssdm  6500  tfrcllembfn  6501  tfrcllemaccex  6505  tfrcllemres  6506  tfrcl  6508  rdgon  6530  frecabcl  6543  pw2f1odclem  6991  undifdcss  7081  ctssdclemn0  7273  ctssdc  7276  nninfninc  7286  nnnninfeq  7291  nnnninfeq2  7292  enomnilem  7301  fodju0  7310  fodjuomnilemres  7311  ismkvnex  7318  fodjumkvlemres  7322  enmkvlem  7324  enwomnilem  7332  nninfdcinf  7334  nninfwlporlem  7336  nninfwlpoimlemdc  7340  nninfinfwlpolem  7341  exmidaclem  7386  exmidontriimlem4  7402  netap  7436  exmidapne  7442  cc2lem  7448  cc3  7450  prltlu  7670  cauappcvgprlemm  7828  caucvgprlemm  7851  caucvgprprlemml  7877  suplocexprlemmu  7901  suplocexprlemdisj  7903  suplocexprlemloc  7904  suplocexprlemub  7906  caucvgsrlemgt1  7978  caucvgsr  7985  suplocsrlemb  7989  suplocsrlempr  7990  suplocsrlem  7991  axcaucvglemcau  8081  axcaucvglemres  8082  axpre-suploclemres  8084  irrmulap  9839  suprzubdc  10451  nninfdcex  10452  zsupssdc  10453  exbtwnzlemstep  10462  apbtwnz  10489  frecuzrdgsuc  10631  frecuzrdgg  10633  frecuzrdgsuctlem  10640  uzsinds  10661  iseqovex  10675  seq3val  10677  seqvalcd  10678  seq3-1  10679  seqf  10681  seq3p1  10682  seqovcd  10684  seqp1cd  10687  seq3clss  10688  seq3fveq2  10692  seqfveq2g  10694  seqfveqg  10695  seq3fveq  10696  seq3feq  10697  seq3shft2  10698  seqshft2g  10699  monoord  10702  monoord2  10703  ser3mono  10704  seq3split  10705  seqsplitg  10706  seq3caopr3  10708  seqcaopr3g  10709  iseqf1olemkle  10714  iseqf1olemklt  10715  iseqf1olemjpcl  10725  iseqf1olemqpcl  10726  iseqf1olemfvp  10727  seq3f1olemqsumkj  10728  seq3f1olemqsum  10730  seq3f1oleml  10733  seq3f1o  10734  seqf1og  10738  seq3id3  10741  seq3id  10742  seq3id2  10743  seq3homo  10744  seq3z  10745  seqhomog  10747  seqfeq4g  10748  ser3ge0  10753  nn0ltexp2  10926  zfz1isolemiso  11056  wrdind  11249  seq3shft  11344  cvg1nlemcau  11490  cvg1nlemres  11491  recvguniq  11501  resqrexlemgt0  11526  resqrexlemoverl  11527  resqrexlemglsq  11528  climi  11793  climcn1  11814  serf0  11858  fsum3cvg  11884  summodclem2  11888  summodc  11889  fsum3  11893  isumz  11895  fsumf1o  11896  isumss  11897  fisumss  11898  isumss2  11899  fsum3cvg2  11900  fsum3cvg3  11902  fsum3ser  11903  fsumsplit  11913  fsumm1  11922  fsum1p  11924  fisumcom2  11944  fsumge1  11967  telfsumo  11972  telfsumo2  11973  fsumparts  11976  isumshft  11996  isum1p  11998  isumnn0nn  11999  isumrpcl  12000  cvgratnnlemnexp  12030  cvgratnnlemmn  12031  cvgratnnlemseq  12032  cvgratnnlemabsle  12033  cvgratnnlemfm  12035  cvgratnnlemrate  12036  cvgratnn  12037  cvgratz  12038  mertenslemi1  12041  mertenslem2  12042  mertensabs  12043  fproddccvg  12078  prodmodclem2a  12082  prodmodc  12084  zproddc  12085  fprodseq  12089  prod1dc  12092  fprodf1o  12094  prodssdc  12095  fprodssdc  12096  fprodm1  12104  fprod1p  12105  fprodcom2fi  12132  sinltxirr  12267  bezoutlemmain  12514  bezoutlemex  12517  bezoutlemzz  12518  bezoutlemmo  12522  bezoutlemle  12524  bezoutlemsup  12525  nnmindc  12550  nnminle  12551  uzwodc  12553  nninfctlemfo  12556  prmind2  12637  isprm5lem  12658  isprm5  12659  pcmpt2  12862  prmpwdvds  12873  ennnfonelemk  12966  ennnfonelemex  12980  ennnfonelemnn0  12988  ctinfomlemom  12993  ctiunctlemudc  13003  ssnnctlemct  13012  nninfdclemcl  13014  nninfdclemp1  13016  nninfdc  13019  prdsbasprj  13310  lidrideqd  13409  grpinvalem  13413  grpinva  13414  grpidd2  13569  mulgsubcl  13668  issubg4m  13725  ghmf1  13805  gsumfzmhm2  13876  lringuplu  14154  mplsubgfilemcl  14657  icnpimaex  14879  lmcvg  14885  lmff  14917  cnmpt11  14951  cnmpt21  14959  comet  15167  dedekindeulemuub  15285  dedekindeulemloc  15287  dedekindeulemlu  15289  dedekindeulemeu  15290  suplociccreex  15292  suplociccex  15293  dedekindicclemuub  15294  dedekindicclemloc  15296  dedekindicclemlu  15298  dedekindicclemeu  15299  dedekindicc  15301  ivthinclemlopn  15304  ivthinclemlr  15305  ivthinclemuopn  15306  ivthinclemur  15307  ivthinclemdisj  15308  ivthinclemloc  15309  ivthinc  15311  ivthdec  15312  ivthreinc  15313  dich0  15320  limcimolemlt  15332  limcimo  15333  cnplimclemr  15337  cnlimci  15341  cnmptlimc  15342  limccnpcntop  15343  limccoap  15346  dvcoapbr  15375  eflt  15443  sin0pilem2  15450  pilem3  15451  perfectlem2  15668  lgsval2lem  15683  lgsdirnn0  15720  lgsdinn0  15721  2sqlem10  15798  2omap  16318  subctctexmid  16325  pw1nct  16328  nnsf  16330  nninfalllem1  16333  nninfsellemeqinf  16341  isomninnlem  16357  trilpolemlt1  16368  trirec0  16371  apdiff  16375  iswomninnlem  16376  ismkvnnlem  16379  redcwlpolemeq1  16381  redc0  16384  reap0  16385  cndcap  16386  dceqnconst  16387  dcapnconst  16388  nconstwlpolem0  16390  nconstwlpolem  16392  neap0mkv  16396  ltlenmkv  16397