Theorem rspcdva 2870

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 2861	. 2 ⊢ (𝐶 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝜓 → 𝜒))
5	1, 2, 4	sylc 62	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364   ∈ wcel 2164  ∀wral 2472

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-v 2762

This theorem is referenced by:  frirrg  4382  wetriext  4610  tfisi  4620  omsinds  4655  suppssov1  6129  caofref  6156  caofinvl  6157  caofdig  6161  oprssdmm  6226  tfrlem1  6363  tfrlem5  6369  tfr1onlemsucfn  6395  tfr1onlemsucaccv  6396  tfr1onlembxssdm  6398  tfr1onlembfn  6399  tfr1onlemaccex  6403  tfr1onlemres  6404  tfrcllemsucfn  6408  tfrcllemsucaccv  6409  tfrcllembxssdm  6411  tfrcllembfn  6412  tfrcllemaccex  6416  tfrcllemres  6417  tfrcl  6419  rdgon  6441  frecabcl  6454  pw2f1odclem  6892  undifdcss  6981  ctssdclemn0  7171  ctssdc  7174  nninfninc  7184  nnnninfeq  7189  nnnninfeq2  7190  enomnilem  7199  fodju0  7208  fodjuomnilemres  7209  ismkvnex  7216  fodjumkvlemres  7220  enmkvlem  7222  enwomnilem  7230  nninfdcinf  7232  nninfwlporlem  7234  nninfwlpoimlemdc  7238  exmidaclem  7270  exmidontriimlem4  7286  netap  7316  exmidapne  7322  cc2lem  7328  cc3  7330  prltlu  7549  cauappcvgprlemm  7707  caucvgprlemm  7730  caucvgprprlemml  7756  suplocexprlemmu  7780  suplocexprlemdisj  7782  suplocexprlemloc  7783  suplocexprlemub  7785  caucvgsrlemgt1  7857  caucvgsr  7864  suplocsrlemb  7868  suplocsrlempr  7869  suplocsrlem  7870  axcaucvglemcau  7960  axcaucvglemres  7961  axpre-suploclemres  7963  irrmulap  9716  exbtwnzlemstep  10319  apbtwnz  10346  frecuzrdgsuc  10488  frecuzrdgg  10490  frecuzrdgsuctlem  10497  uzsinds  10518  iseqovex  10532  seq3val  10534  seqvalcd  10535  seq3-1  10536  seqf  10538  seq3p1  10539  seqovcd  10541  seqp1cd  10544  seq3clss  10545  seq3fveq2  10549  seqfveq2g  10551  seqfveqg  10552  seq3fveq  10553  seq3feq  10554  seq3shft2  10555  seqshft2g  10556  monoord  10559  monoord2  10560  ser3mono  10561  seq3split  10562  seqsplitg  10563  seq3caopr3  10565  seqcaopr3g  10566  iseqf1olemkle  10571  iseqf1olemklt  10572  iseqf1olemjpcl  10582  iseqf1olemqpcl  10583  iseqf1olemfvp  10584  seq3f1olemqsumkj  10585  seq3f1olemqsum  10587  seq3f1oleml  10590  seq3f1o  10591  seqf1og  10595  seq3id3  10598  seq3id  10599  seq3id2  10600  seq3homo  10601  seq3z  10602  seqhomog  10604  seqfeq4g  10605  ser3ge0  10610  nn0ltexp2  10783  zfz1isolemiso  10913  seq3shft  10985  cvg1nlemcau  11131  cvg1nlemres  11132  recvguniq  11142  resqrexlemgt0  11167  resqrexlemoverl  11168  resqrexlemglsq  11169  climi  11433  climcn1  11454  serf0  11498  fsum3cvg  11524  summodclem2  11528  summodc  11529  fsum3  11533  isumz  11535  fsumf1o  11536  isumss  11537  fisumss  11538  isumss2  11539  fsum3cvg2  11540  fsum3cvg3  11542  fsum3ser  11543  fsumsplit  11553  fsumm1  11562  fsum1p  11564  fisumcom2  11584  fsumge1  11607  telfsumo  11612  telfsumo2  11613  fsumparts  11616  isumshft  11636  isum1p  11638  isumnn0nn  11639  isumrpcl  11640  cvgratnnlemnexp  11670  cvgratnnlemmn  11671  cvgratnnlemseq  11672  cvgratnnlemabsle  11673  cvgratnnlemfm  11675  cvgratnnlemrate  11676  cvgratnn  11677  cvgratz  11678  mertenslemi1  11681  mertenslem2  11682  mertensabs  11683  fproddccvg  11718  prodmodclem2a  11722  prodmodc  11724  zproddc  11725  fprodseq  11729  prod1dc  11732  fprodf1o  11734  prodssdc  11735  fprodssdc  11736  fprodm1  11744  fprod1p  11745  fprodcom2fi  11772  sinltxirr  11907  suprzubdc  12092  nninfdcex  12093  zsupssdc  12094  bezoutlemmain  12138  bezoutlemex  12141  bezoutlemzz  12142  bezoutlemmo  12146  bezoutlemle  12148  bezoutlemsup  12149  nnmindc  12174  nnminle  12175  uzwodc  12177  nninfctlemfo  12180  prmind2  12261  isprm5lem  12282  isprm5  12283  pcmpt2  12485  prmpwdvds  12496  ennnfonelemk  12560  ennnfonelemex  12574  ennnfonelemnn0  12582  ctinfomlemom  12587  ctiunctlemudc  12597  ssnnctlemct  12606  nninfdclemcl  12608  nninfdclemp1  12610  nninfdc  12613  lidrideqd  12967  grpinvalem  12971  grpinva  12972  grpidd2  13116  mulgsubcl  13209  issubg4m  13266  ghmf1  13346  gsumfzmhm2  13417  lringuplu  13695  icnpimaex  14390  lmcvg  14396  lmff  14428  cnmpt11  14462  cnmpt21  14470  comet  14678  dedekindeulemuub  14796  dedekindeulemloc  14798  dedekindeulemlu  14800  dedekindeulemeu  14801  suplociccreex  14803  suplociccex  14804  dedekindicclemuub  14805  dedekindicclemloc  14807  dedekindicclemlu  14809  dedekindicclemeu  14810  dedekindicc  14812  ivthinclemlopn  14815  ivthinclemlr  14816  ivthinclemuopn  14817  ivthinclemur  14818  ivthinclemdisj  14819  ivthinclemloc  14820  ivthinc  14822  ivthdec  14823  ivthreinc  14824  dich0  14831  limcimolemlt  14843  limcimo  14844  cnplimclemr  14848  cnlimci  14852  cnmptlimc  14853  limccnpcntop  14854  limccoap  14857  dvcoapbr  14886  eflt  14951  sin0pilem2  14958  pilem3  14959  lgsval2lem  15167  lgsdirnn0  15204  lgsdinn0  15205  2sqlem10  15282  subctctexmid  15561  pw1nct  15563  nnsf  15565  nninfalllem1  15568  nninfsellemeqinf  15576  isomninnlem  15590  trilpolemlt1  15601  trirec0  15604  apdiff  15608  iswomninnlem  15609  ismkvnnlem  15612  redcwlpolemeq1  15614  redc0  15617  reap0  15618  cndcap  15619  dceqnconst  15620  dcapnconst  15621  nconstwlpolem0  15623  nconstwlpolem  15625  neap0mkv  15629  ltlenmkv  15630