Theorem rspcdva 2913

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 2904	. 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 2802

This theorem is referenced by:  frirrg  4443  wetriext  4671  tfisi  4681  omsinds  4716  suppssov1  6225  caofref  6253  caofinvl  6254  caofdig  6262  oprssdmm  6327  tfrlem1  6467  tfrlem5  6473  tfr1onlemsucfn  6499  tfr1onlemsucaccv  6500  tfr1onlembxssdm  6502  tfr1onlembfn  6503  tfr1onlemaccex  6507  tfr1onlemres  6508  tfrcllemsucfn  6512  tfrcllemsucaccv  6513  tfrcllembxssdm  6515  tfrcllembfn  6516  tfrcllemaccex  6520  tfrcllemres  6521  tfrcl  6523  rdgon  6545  frecabcl  6558  pw2f1odclem  7013  elssdc  7085  undifdcss  7106  ctssdclemn0  7298  ctssdc  7301  nninfninc  7311  nnnninfeq  7316  nnnninfeq2  7317  enomnilem  7326  fodju0  7335  fodjuomnilemres  7336  ismkvnex  7343  fodjumkvlemres  7347  enmkvlem  7349  enwomnilem  7357  nninfdcinf  7359  nninfwlporlem  7361  nninfwlpoimlemdc  7365  nninfinfwlpolem  7366  exmidaclem  7411  exmidontriimlem4  7427  netap  7461  exmidapne  7467  cc2lem  7473  cc3  7475  prltlu  7695  cauappcvgprlemm  7853  caucvgprlemm  7876  caucvgprprlemml  7902  suplocexprlemmu  7926  suplocexprlemdisj  7928  suplocexprlemloc  7929  suplocexprlemub  7931  caucvgsrlemgt1  8003  caucvgsr  8010  suplocsrlemb  8014  suplocsrlempr  8015  suplocsrlem  8016  axcaucvglemcau  8106  axcaucvglemres  8107  axpre-suploclemres  8109  irrmulap  9870  suprzubdc  10484  nninfdcex  10485  zsupssdc  10486  exbtwnzlemstep  10495  apbtwnz  10522  frecuzrdgsuc  10664  frecuzrdgg  10666  frecuzrdgsuctlem  10673  uzsinds  10694  iseqovex  10708  seq3val  10710  seqvalcd  10711  seq3-1  10712  seqf  10714  seq3p1  10715  seqovcd  10717  seqp1cd  10720  seq3clss  10721  seq3fveq2  10725  seqfveq2g  10727  seqfveqg  10728  seq3fveq  10729  seq3feq  10730  seq3shft2  10731  seqshft2g  10732  monoord  10735  monoord2  10736  ser3mono  10737  seq3split  10738  seqsplitg  10739  seq3caopr3  10741  seqcaopr3g  10742  iseqf1olemkle  10747  iseqf1olemklt  10748  iseqf1olemjpcl  10758  iseqf1olemqpcl  10759  iseqf1olemfvp  10760  seq3f1olemqsumkj  10761  seq3f1olemqsum  10763  seq3f1oleml  10766  seq3f1o  10767  seqf1og  10771  seq3id3  10774  seq3id  10775  seq3id2  10776  seq3homo  10777  seq3z  10778  seqhomog  10780  seqfeq4g  10781  ser3ge0  10786  nn0ltexp2  10959  zfz1isolemiso  11090  wrdind  11290  seq3shft  11386  cvg1nlemcau  11532  cvg1nlemres  11533  recvguniq  11543  resqrexlemgt0  11568  resqrexlemoverl  11569  resqrexlemglsq  11570  climi  11835  climcn1  11856  serf0  11900  fsum3cvg  11926  summodclem2  11930  summodc  11931  fsum3  11935  isumz  11937  fsumf1o  11938  isumss  11939  fisumss  11940  isumss2  11941  fsum3cvg2  11942  fsum3cvg3  11944  fsum3ser  11945  fsumsplit  11955  fsumm1  11964  fsum1p  11966  fisumcom2  11986  fsumge1  12009  telfsumo  12014  telfsumo2  12015  fsumparts  12018  isumshft  12038  isum1p  12040  isumnn0nn  12041  isumrpcl  12042  cvgratnnlemnexp  12072  cvgratnnlemmn  12073  cvgratnnlemseq  12074  cvgratnnlemabsle  12075  cvgratnnlemfm  12077  cvgratnnlemrate  12078  cvgratnn  12079  cvgratz  12080  mertenslemi1  12083  mertenslem2  12084  mertensabs  12085  fproddccvg  12120  prodmodclem2a  12124  prodmodc  12126  zproddc  12127  fprodseq  12131  prod1dc  12134  fprodf1o  12136  prodssdc  12137  fprodssdc  12138  fprodm1  12146  fprod1p  12147  fprodcom2fi  12174  sinltxirr  12309  bezoutlemmain  12556  bezoutlemex  12559  bezoutlemzz  12560  bezoutlemmo  12564  bezoutlemle  12566  bezoutlemsup  12567  nnmindc  12592  nnminle  12593  uzwodc  12595  nninfctlemfo  12598  prmind2  12679  isprm5lem  12700  isprm5  12701  pcmpt2  12904  prmpwdvds  12915  ennnfonelemk  13008  ennnfonelemex  13022  ennnfonelemnn0  13030  ctinfomlemom  13035  ctiunctlemudc  13045  ssnnctlemct  13054  nninfdclemcl  13056  nninfdclemp1  13058  nninfdc  13061  prdsbasprj  13352  lidrideqd  13451  grpinvalem  13455  grpinva  13456  grpidd2  13611  mulgsubcl  13710  issubg4m  13767  ghmf1  13847  gsumfzmhm2  13918  lringuplu  14197  mplsubgfilemcl  14700  icnpimaex  14922  lmcvg  14928  lmff  14960  cnmpt11  14994  cnmpt21  15002  comet  15210  dedekindeulemuub  15328  dedekindeulemloc  15330  dedekindeulemlu  15332  dedekindeulemeu  15333  suplociccreex  15335  suplociccex  15336  dedekindicclemuub  15337  dedekindicclemloc  15339  dedekindicclemlu  15341  dedekindicclemeu  15342  dedekindicc  15344  ivthinclemlopn  15347  ivthinclemlr  15348  ivthinclemuopn  15349  ivthinclemur  15350  ivthinclemdisj  15351  ivthinclemloc  15352  ivthinc  15354  ivthdec  15355  ivthreinc  15356  dich0  15363  limcimolemlt  15375  limcimo  15376  cnplimclemr  15380  cnlimci  15384  cnmptlimc  15385  limccnpcntop  15386  limccoap  15389  dvcoapbr  15418  eflt  15486  sin0pilem2  15493  pilem3  15494  perfectlem2  15711  lgsval2lem  15726  lgsdirnn0  15763  lgsdinn0  15764  2sqlem10  15841  2omap  16504  subctctexmid  16511  pw1nct  16514  nnsf  16517  nninfalllem1  16520  nninfsellemeqinf  16528  isomninnlem  16544  trilpolemlt1  16555  trirec0  16558  apdiff  16562  iswomninnlem  16563  ismkvnnlem  16566  redcwlpolemeq1  16568  redc0  16571  reap0  16572  cndcap  16573  dceqnconst  16574  dcapnconst  16575  nconstwlpolem0  16577  nconstwlpolem  16579  neap0mkv  16583  ltlenmkv  16584