Theorem rspcdva 2873

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

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

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-v 2765

This theorem is referenced by:  frirrg  4386  wetriext  4614  tfisi  4624  omsinds  4659  suppssov1  6136  caofref  6164  caofinvl  6165  caofdig  6173  oprssdmm  6238  tfrlem1  6375  tfrlem5  6381  tfr1onlemsucfn  6407  tfr1onlemsucaccv  6408  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfr1onlemaccex  6415  tfr1onlemres  6416  tfrcllemsucfn  6420  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllembfn  6424  tfrcllemaccex  6428  tfrcllemres  6429  tfrcl  6431  rdgon  6453  frecabcl  6466  pw2f1odclem  6904  undifdcss  6993  ctssdclemn0  7185  ctssdc  7188  nninfninc  7198  nnnninfeq  7203  nnnninfeq2  7204  enomnilem  7213  fodju0  7222  fodjuomnilemres  7223  ismkvnex  7230  fodjumkvlemres  7234  enmkvlem  7236  enwomnilem  7244  nninfdcinf  7246  nninfwlporlem  7248  nninfwlpoimlemdc  7252  nninfinfwlpolem  7253  exmidaclem  7293  exmidontriimlem4  7309  netap  7339  exmidapne  7345  cc2lem  7351  cc3  7353  prltlu  7573  cauappcvgprlemm  7731  caucvgprlemm  7754  caucvgprprlemml  7780  suplocexprlemmu  7804  suplocexprlemdisj  7806  suplocexprlemloc  7807  suplocexprlemub  7809  caucvgsrlemgt1  7881  caucvgsr  7888  suplocsrlemb  7892  suplocsrlempr  7893  suplocsrlem  7894  axcaucvglemcau  7984  axcaucvglemres  7985  axpre-suploclemres  7987  irrmulap  9741  suprzubdc  10345  nninfdcex  10346  zsupssdc  10347  exbtwnzlemstep  10356  apbtwnz  10383  frecuzrdgsuc  10525  frecuzrdgg  10527  frecuzrdgsuctlem  10534  uzsinds  10555  iseqovex  10569  seq3val  10571  seqvalcd  10572  seq3-1  10573  seqf  10575  seq3p1  10576  seqovcd  10578  seqp1cd  10581  seq3clss  10582  seq3fveq2  10586  seqfveq2g  10588  seqfveqg  10589  seq3fveq  10590  seq3feq  10591  seq3shft2  10592  seqshft2g  10593  monoord  10596  monoord2  10597  ser3mono  10598  seq3split  10599  seqsplitg  10600  seq3caopr3  10602  seqcaopr3g  10603  iseqf1olemkle  10608  iseqf1olemklt  10609  iseqf1olemjpcl  10619  iseqf1olemqpcl  10620  iseqf1olemfvp  10621  seq3f1olemqsumkj  10622  seq3f1olemqsum  10624  seq3f1oleml  10627  seq3f1o  10628  seqf1og  10632  seq3id3  10635  seq3id  10636  seq3id2  10637  seq3homo  10638  seq3z  10639  seqhomog  10641  seqfeq4g  10642  ser3ge0  10647  nn0ltexp2  10820  zfz1isolemiso  10950  seq3shft  11022  cvg1nlemcau  11168  cvg1nlemres  11169  recvguniq  11179  resqrexlemgt0  11204  resqrexlemoverl  11205  resqrexlemglsq  11206  climi  11471  climcn1  11492  serf0  11536  fsum3cvg  11562  summodclem2  11566  summodc  11567  fsum3  11571  isumz  11573  fsumf1o  11574  isumss  11575  fisumss  11576  isumss2  11577  fsum3cvg2  11578  fsum3cvg3  11580  fsum3ser  11581  fsumsplit  11591  fsumm1  11600  fsum1p  11602  fisumcom2  11622  fsumge1  11645  telfsumo  11650  telfsumo2  11651  fsumparts  11654  isumshft  11674  isum1p  11676  isumnn0nn  11677  isumrpcl  11678  cvgratnnlemnexp  11708  cvgratnnlemmn  11709  cvgratnnlemseq  11710  cvgratnnlemabsle  11711  cvgratnnlemfm  11713  cvgratnnlemrate  11714  cvgratnn  11715  cvgratz  11716  mertenslemi1  11719  mertenslem2  11720  mertensabs  11721  fproddccvg  11756  prodmodclem2a  11760  prodmodc  11762  zproddc  11763  fprodseq  11767  prod1dc  11770  fprodf1o  11772  prodssdc  11773  fprodssdc  11774  fprodm1  11782  fprod1p  11783  fprodcom2fi  11810  sinltxirr  11945  bezoutlemmain  12192  bezoutlemex  12195  bezoutlemzz  12196  bezoutlemmo  12200  bezoutlemle  12202  bezoutlemsup  12203  nnmindc  12228  nnminle  12229  uzwodc  12231  nninfctlemfo  12234  prmind2  12315  isprm5lem  12336  isprm5  12337  pcmpt2  12540  prmpwdvds  12551  ennnfonelemk  12644  ennnfonelemex  12658  ennnfonelemnn0  12666  ctinfomlemom  12671  ctiunctlemudc  12681  ssnnctlemct  12690  nninfdclemcl  12692  nninfdclemp1  12694  nninfdc  12697  prdsbasprj  12986  lidrideqd  13085  grpinvalem  13089  grpinva  13090  grpidd2  13245  mulgsubcl  13344  issubg4m  13401  ghmf1  13481  gsumfzmhm2  13552  lringuplu  13830  mplsubgfilemcl  14333  icnpimaex  14555  lmcvg  14561  lmff  14593  cnmpt11  14627  cnmpt21  14635  comet  14843  dedekindeulemuub  14961  dedekindeulemloc  14963  dedekindeulemlu  14965  dedekindeulemeu  14966  suplociccreex  14968  suplociccex  14969  dedekindicclemuub  14970  dedekindicclemloc  14972  dedekindicclemlu  14974  dedekindicclemeu  14975  dedekindicc  14977  ivthinclemlopn  14980  ivthinclemlr  14981  ivthinclemuopn  14982  ivthinclemur  14983  ivthinclemdisj  14984  ivthinclemloc  14985  ivthinc  14987  ivthdec  14988  ivthreinc  14989  dich0  14996  limcimolemlt  15008  limcimo  15009  cnplimclemr  15013  cnlimci  15017  cnmptlimc  15018  limccnpcntop  15019  limccoap  15022  dvcoapbr  15051  eflt  15119  sin0pilem2  15126  pilem3  15127  perfectlem2  15344  lgsval2lem  15359  lgsdirnn0  15396  lgsdinn0  15397  2sqlem10  15474  2omap  15750  subctctexmid  15755  pw1nct  15758  nnsf  15760  nninfalllem1  15763  nninfsellemeqinf  15771  isomninnlem  15787  trilpolemlt1  15798  trirec0  15801  apdiff  15805  iswomninnlem  15806  ismkvnnlem  15809  redcwlpolemeq1  15811  redc0  15814  reap0  15815  cndcap  15816  dceqnconst  15817  dcapnconst  15818  nconstwlpolem0  15820  nconstwlpolem  15822  neap0mkv  15826  ltlenmkv  15827