Theorem rspcdva 2928

Description: Restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 21-Jun-2020.)

Hypotheses

Ref	Expression
rspcdva.1	|- ( x = C -> ( ps <-> ch ) )
rspcdva.2	|- ( ph -> A. x e. A ps )
rspcdva.3	|- ( ph -> C e. A )

Assertion

Ref	Expression
rspcdva	|- ( ph -> ch )

Distinct variable groups:   x, A   x, C   ch, x

Allowed substitution hints:   ph( x)   ps( x)

Proof of Theorem rspcdva

Step	Hyp	Ref	Expression
1		rspcdva.3	. 2 |- ( ph -> C e. A )
2		rspcdva.2	. 2 |- ( ph -> A. x e. A ps )
3		rspcdva.1	. . 3 |- ( x = C -> ( ps <-> ch ) )
4	3	rspcv 2919	. 2 |- ( C e. A -> ( A. x e. A ps -> ch ) )
5	1, 2, 4	sylc 62	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1398   e. wcel 2205   A.wral 2522

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-v 2817

This theorem is referenced by:  frirrg  4477  wetriext  4706  tfisi  4716  omsinds  4751  suppssov1  6274  caofref  6302  caofinvl  6303  caofdig  6311  oprssdmm  6380  suppssdc  6475  suppssrst  6476  suppssrgst  6477  suppofss1dcl  6479  suppofss2dcl  6480  tfrlem1  6554  tfrlem5  6560  tfr1onlemsucfn  6586  tfr1onlemsucaccv  6587  tfr1onlembxssdm  6589  tfr1onlembfn  6590  tfr1onlemaccex  6594  tfr1onlemres  6595  tfrcllemsucfn  6599  tfrcllemsucaccv  6600  tfrcllembxssdm  6602  tfrcllembfn  6603  tfrcllemaccex  6607  tfrcllemres  6608  tfrcl  6610  rdgon  6632  frecabcl  6645  pw2f1odclem  7102  elssdc  7177  undifdcss  7198  2omap  7284  ctssdclemn0  7416  ctssdc  7419  nninfninc  7429  nnnninfeq  7434  nnnninfeq2  7435  enomnilem  7444  fodju0  7453  fodjuomnilemres  7454  ismkvnex  7461  fodjumkvlemres  7465  enmkvlem  7467  enwomnilem  7475  nninfdcinf  7477  nninfwlporlem  7479  nninfwlpoimlemdc  7483  nninfinfwlpolem  7484  exmidaclem  7530  exmidontriimlem4  7546  papirr  7577  papsym  7578  papcotr  7579  netap  7586  exmidapne  7592  cc2lem  7598  cc3  7600  prltlu  7820  cauappcvgprlemm  7978  caucvgprlemm  8001  caucvgprprlemml  8027  suplocexprlemmu  8051  suplocexprlemdisj  8053  suplocexprlemloc  8054  suplocexprlemub  8056  caucvgsrlemgt1  8128  caucvgsr  8135  suplocsrlemb  8139  suplocsrlempr  8140  suplocsrlem  8141  axcaucvglemcau  8231  axcaucvglemres  8232  axpre-suploclemres  8234  irrmulap  10003  suprzubdc  10625  nninfdcex  10626  zsupssdc  10627  exbtwnzlemstep  10636  apbtwnz  10663  frecuzrdgsuc  10805  frecuzrdgg  10807  frecuzrdgsuctlem  10814  uzsinds  10835  iseqovex  10849  seq3val  10851  seqvalcd  10852  seq3-1  10853  seqf  10855  seq3p1  10856  seqovcd  10858  seqp1cd  10861  seq3clss  10862  seq3fveq2  10866  seqfveq2g  10868  seqfveqg  10869  seq3fveq  10870  seq3feq  10871  seq3shft2  10872  seqshft2g  10873  monoord  10876  monoord2  10877  ser3mono  10878  seq3split  10879  seqsplitg  10880  seq3caopr3  10882  seqcaopr3g  10883  iseqf1olemkle  10888  iseqf1olemklt  10889  iseqf1olemjpcl  10899  iseqf1olemqpcl  10900  iseqf1olemfvp  10901  seq3f1olemqsumkj  10902  seq3f1olemqsum  10904  seq3f1oleml  10907  seq3f1o  10908  seqf1og  10912  seq3id3  10915  seq3id  10916  seq3id2  10917  seq3homo  10918  seq3z  10919  seqhomog  10921  seqfeq4g  10922  ser3ge0  10927  nn0ltexp2  11101  hashfibclem  11236  zfz1isolemiso  11241  wrdind  11444  seq3shft  11553  cvg1nlemcau  11700  cvg1nlemres  11701  recvguniq  11711  resqrexlemgt0  11736  resqrexlemoverl  11737  resqrexlemglsq  11738  climi  12003  climcn1  12024  serf0  12068  fsum3cvg  12095  summodclem2  12099  summodc  12100  fsum3  12104  isumz  12106  fsumf1o  12107  isumss  12108  fisumss  12109  isumss2  12110  fsum3cvg2  12111  fsum3cvg3  12113  fsum3ser  12114  fsumsplit  12124  fsumm1  12133  fsum1p  12135  fisumcom2  12155  fsumge1  12178  telfsumo  12183  telfsumo2  12184  fsumparts  12187  isumshft  12207  isum1p  12209  isumnn0nn  12210  isumrpcl  12211  cvgratnnlemnexp  12241  cvgratnnlemmn  12242  cvgratnnlemseq  12243  cvgratnnlemabsle  12244  cvgratnnlemfm  12246  cvgratnnlemrate  12247  cvgratnn  12248  cvgratz  12249  mertenslemi1  12252  mertenslem2  12253  mertensabs  12254  fproddccvg  12289  prodmodclem2a  12293  prodmodc  12295  zproddc  12296  fprodseq  12300  prod1dc  12303  fprodf1o  12305  prodssdc  12306  fprodssdc  12307  fprodm1  12315  fprod1p  12316  fprodcom2fi  12343  sinltxirr  12478  bezoutlemmain  12725  bezoutlemex  12728  bezoutlemzz  12729  bezoutlemmo  12733  bezoutlemle  12735  bezoutlemsup  12736  nnmindc  12761  nnminle  12762  uzwodc  12764  nninfctlemfo  12767  prmind2  12848  isprm5lem  12869  isprm5  12870  pcmpt2  13073  prmpwdvds  13084  ennnfonelemk  13241  ennnfonelemex  13255  ennnfonelemnn0  13263  ctinfomlemom  13268  ctiunctlemudc  13278  ssnnctlemct  13287  nninfdclemcl  13289  nninfdclemp1  13291  nninfdc  13294  lidrideqd  13650  grpinvalem  13654  grpinva  13655  grpidd2  13795  mulgsubcl  13888  issubg4m  13945  ghmf1  14025  gzsummhm2  14095  gsummhm2fi  14114  prdsbasprj  14131  lringuplu  14448  mplsubgfilemcl  14985  icnpimaex  15207  lmcvg  15213  lmff  15245  cnmpt11  15279  cnmpt21  15287  comet  15495  dedekindeulemuub  15613  dedekindeulemloc  15615  dedekindeulemlu  15617  dedekindeulemeu  15618  suplociccreex  15620  suplociccex  15621  dedekindicclemuub  15622  dedekindicclemloc  15624  dedekindicclemlu  15626  dedekindicclemeu  15627  dedekindicc  15629  ivthinclemlopn  15632  ivthinclemlr  15633  ivthinclemuopn  15634  ivthinclemur  15635  ivthinclemdisj  15636  ivthinclemloc  15637  ivthinc  15639  ivthdec  15640  ivthreinc  15641  dich0  15648  limcimolemlt  15660  limcimo  15661  cnplimclemr  15665  cnlimci  15669  cnmptlimc  15670  limccnpcntop  15671  limccoap  15674  dvcoapbr  15703  eflt  15771  sin0pilem2  15778  pilem3  15779  perfectlem2  16000  lgsval2lem  16015  lgsdirnn0  16052  lgsdinn0  16053  2sqlem10  16130  eupth2lem3fi  16603  subctctexmid  16916  pw1nct  16919  exmidnotnotr  16921  exmidcon  16922  exmidpeirce  16923  nnsf  16925  nninfalllem1  16928  nninfsellemeqinf  16936  isomninnlem  16956  trilpolemlt1  16967  trirec0  16970  apdiff  16974  iswomninnlem  16976  ismkvnnlem  16979  redcwlpolemeq1  16981  redc0  16984  reap0  16985  cndcap  16986  dceqnconst  16987  dcapnconst  16988  nconstwlpolem0  16990  nconstwlpolem  16992  neap0mkv  16996  ltlenmkv  16997