Theorem rspcdva 2915

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 2906	. 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 1397   e. wcel 2202   A.wral 2510

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-v 2804

This theorem is referenced by:  frirrg  4447  wetriext  4675  tfisi  4685  omsinds  4720  suppssov1  6232  caofref  6260  caofinvl  6261  caofdig  6269  oprssdmm  6334  tfrlem1  6474  tfrlem5  6480  tfr1onlemsucfn  6506  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfr1onlemaccex  6514  tfr1onlemres  6515  tfrcllemsucfn  6519  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllembfn  6523  tfrcllemaccex  6527  tfrcllemres  6528  tfrcl  6530  rdgon  6552  frecabcl  6565  pw2f1odclem  7020  elssdc  7094  undifdcss  7115  ctssdclemn0  7309  ctssdc  7312  nninfninc  7322  nnnninfeq  7327  nnnninfeq2  7328  enomnilem  7337  fodju0  7346  fodjuomnilemres  7347  ismkvnex  7354  fodjumkvlemres  7358  enmkvlem  7360  enwomnilem  7368  nninfdcinf  7370  nninfwlporlem  7372  nninfwlpoimlemdc  7376  nninfinfwlpolem  7377  exmidaclem  7423  exmidontriimlem4  7439  netap  7473  exmidapne  7479  cc2lem  7485  cc3  7487  prltlu  7707  cauappcvgprlemm  7865  caucvgprlemm  7888  caucvgprprlemml  7914  suplocexprlemmu  7938  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemub  7943  caucvgsrlemgt1  8015  caucvgsr  8022  suplocsrlemb  8026  suplocsrlempr  8027  suplocsrlem  8028  axcaucvglemcau  8118  axcaucvglemres  8119  axpre-suploclemres  8121  irrmulap  9882  suprzubdc  10497  nninfdcex  10498  zsupssdc  10499  exbtwnzlemstep  10508  apbtwnz  10535  frecuzrdgsuc  10677  frecuzrdgg  10679  frecuzrdgsuctlem  10686  uzsinds  10707  iseqovex  10721  seq3val  10723  seqvalcd  10724  seq3-1  10725  seqf  10727  seq3p1  10728  seqovcd  10730  seqp1cd  10733  seq3clss  10734  seq3fveq2  10738  seqfveq2g  10740  seqfveqg  10741  seq3fveq  10742  seq3feq  10743  seq3shft2  10744  seqshft2g  10745  monoord  10748  monoord2  10749  ser3mono  10750  seq3split  10751  seqsplitg  10752  seq3caopr3  10754  seqcaopr3g  10755  iseqf1olemkle  10760  iseqf1olemklt  10761  iseqf1olemjpcl  10771  iseqf1olemqpcl  10772  iseqf1olemfvp  10773  seq3f1olemqsumkj  10774  seq3f1olemqsum  10776  seq3f1oleml  10779  seq3f1o  10780  seqf1og  10784  seq3id3  10787  seq3id  10788  seq3id2  10789  seq3homo  10790  seq3z  10791  seqhomog  10793  seqfeq4g  10794  ser3ge0  10799  nn0ltexp2  10972  zfz1isolemiso  11104  wrdind  11307  seq3shft  11416  cvg1nlemcau  11562  cvg1nlemres  11563  recvguniq  11573  resqrexlemgt0  11598  resqrexlemoverl  11599  resqrexlemglsq  11600  climi  11865  climcn1  11886  serf0  11930  fsum3cvg  11957  summodclem2  11961  summodc  11962  fsum3  11966  isumz  11968  fsumf1o  11969  isumss  11970  fisumss  11971  isumss2  11972  fsum3cvg2  11973  fsum3cvg3  11975  fsum3ser  11976  fsumsplit  11986  fsumm1  11995  fsum1p  11997  fisumcom2  12017  fsumge1  12040  telfsumo  12045  telfsumo2  12046  fsumparts  12049  isumshft  12069  isum1p  12071  isumnn0nn  12072  isumrpcl  12073  cvgratnnlemnexp  12103  cvgratnnlemmn  12104  cvgratnnlemseq  12105  cvgratnnlemabsle  12106  cvgratnnlemfm  12108  cvgratnnlemrate  12109  cvgratnn  12110  cvgratz  12111  mertenslemi1  12114  mertenslem2  12115  mertensabs  12116  fproddccvg  12151  prodmodclem2a  12155  prodmodc  12157  zproddc  12158  fprodseq  12162  prod1dc  12165  fprodf1o  12167  prodssdc  12168  fprodssdc  12169  fprodm1  12177  fprod1p  12178  fprodcom2fi  12205  sinltxirr  12340  bezoutlemmain  12587  bezoutlemex  12590  bezoutlemzz  12591  bezoutlemmo  12595  bezoutlemle  12597  bezoutlemsup  12598  nnmindc  12623  nnminle  12624  uzwodc  12626  nninfctlemfo  12629  prmind2  12710  isprm5lem  12731  isprm5  12732  pcmpt2  12935  prmpwdvds  12946  ennnfonelemk  13039  ennnfonelemex  13053  ennnfonelemnn0  13061  ctinfomlemom  13066  ctiunctlemudc  13076  ssnnctlemct  13085  nninfdclemcl  13087  nninfdclemp1  13089  nninfdc  13092  prdsbasprj  13383  lidrideqd  13482  grpinvalem  13486  grpinva  13487  grpidd2  13642  mulgsubcl  13741  issubg4m  13798  ghmf1  13878  gsumfzmhm2  13949  lringuplu  14229  mplsubgfilemcl  14732  icnpimaex  14954  lmcvg  14960  lmff  14992  cnmpt11  15026  cnmpt21  15034  comet  15242  dedekindeulemuub  15360  dedekindeulemloc  15362  dedekindeulemlu  15364  dedekindeulemeu  15365  suplociccreex  15367  suplociccex  15368  dedekindicclemuub  15369  dedekindicclemloc  15371  dedekindicclemlu  15373  dedekindicclemeu  15374  dedekindicc  15376  ivthinclemlopn  15379  ivthinclemlr  15380  ivthinclemuopn  15381  ivthinclemur  15382  ivthinclemdisj  15383  ivthinclemloc  15384  ivthinc  15386  ivthdec  15387  ivthreinc  15388  dich0  15395  limcimolemlt  15407  limcimo  15408  cnplimclemr  15412  cnlimci  15416  cnmptlimc  15417  limccnpcntop  15418  limccoap  15421  dvcoapbr  15450  eflt  15518  sin0pilem2  15525  pilem3  15526  perfectlem2  15743  lgsval2lem  15758  lgsdirnn0  15795  lgsdinn0  15796  2sqlem10  15873  eupth2lem3fi  16346  2omap  16645  subctctexmid  16652  pw1nct  16655  nnsf  16658  nninfalllem1  16661  nninfsellemeqinf  16669  isomninnlem  16685  trilpolemlt1  16696  trirec0  16699  apdiff  16703  iswomninnlem  16705  ismkvnnlem  16708  redcwlpolemeq1  16710  redc0  16713  reap0  16714  cndcap  16715  dceqnconst  16716  dcapnconst  16717  nconstwlpolem0  16719  nconstwlpolem  16721  neap0mkv  16725  ltlenmkv  16726