Theorem rspcdva 2916

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 2907	. 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 2202   A.wral 2511

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 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-v 2805

This theorem is referenced by:  frirrg  4453  wetriext  4681  tfisi  4691  omsinds  4726  suppssov1  6241  caofref  6269  caofinvl  6270  caofdig  6278  oprssdmm  6343  suppssdc  6438  suppssrst  6439  suppssrgst  6440  suppofss1dcl  6442  suppofss2dcl  6443  tfrlem1  6517  tfrlem5  6523  tfr1onlemsucfn  6549  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfr1onlemaccex  6557  tfr1onlemres  6558  tfrcllemsucfn  6562  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllembfn  6566  tfrcllemaccex  6570  tfrcllemres  6571  tfrcl  6573  rdgon  6595  frecabcl  6608  pw2f1odclem  7063  elssdc  7137  undifdcss  7158  ctssdclemn0  7369  ctssdc  7372  nninfninc  7382  nnnninfeq  7387  nnnninfeq2  7388  enomnilem  7397  fodju0  7406  fodjuomnilemres  7407  ismkvnex  7414  fodjumkvlemres  7418  enmkvlem  7420  enwomnilem  7428  nninfdcinf  7430  nninfwlporlem  7432  nninfwlpoimlemdc  7436  nninfinfwlpolem  7437  exmidaclem  7483  exmidontriimlem4  7499  netap  7533  exmidapne  7539  cc2lem  7545  cc3  7547  prltlu  7767  cauappcvgprlemm  7925  caucvgprlemm  7948  caucvgprprlemml  7974  suplocexprlemmu  7998  suplocexprlemdisj  8000  suplocexprlemloc  8001  suplocexprlemub  8003  caucvgsrlemgt1  8075  caucvgsr  8082  suplocsrlemb  8086  suplocsrlempr  8087  suplocsrlem  8088  axcaucvglemcau  8178  axcaucvglemres  8179  axpre-suploclemres  8181  irrmulap  9943  suprzubdc  10559  nninfdcex  10560  zsupssdc  10561  exbtwnzlemstep  10570  apbtwnz  10597  frecuzrdgsuc  10739  frecuzrdgg  10741  frecuzrdgsuctlem  10748  uzsinds  10769  iseqovex  10783  seq3val  10785  seqvalcd  10786  seq3-1  10787  seqf  10789  seq3p1  10790  seqovcd  10792  seqp1cd  10795  seq3clss  10796  seq3fveq2  10800  seqfveq2g  10802  seqfveqg  10803  seq3fveq  10804  seq3feq  10805  seq3shft2  10806  seqshft2g  10807  monoord  10810  monoord2  10811  ser3mono  10812  seq3split  10813  seqsplitg  10814  seq3caopr3  10816  seqcaopr3g  10817  iseqf1olemkle  10822  iseqf1olemklt  10823  iseqf1olemjpcl  10833  iseqf1olemqpcl  10834  iseqf1olemfvp  10835  seq3f1olemqsumkj  10836  seq3f1olemqsum  10838  seq3f1oleml  10841  seq3f1o  10842  seqf1og  10846  seq3id3  10849  seq3id  10850  seq3id2  10851  seq3homo  10852  seq3z  10853  seqhomog  10855  seqfeq4g  10856  ser3ge0  10861  nn0ltexp2  11034  zfz1isolemiso  11166  wrdind  11369  seq3shft  11478  cvg1nlemcau  11624  cvg1nlemres  11625  recvguniq  11635  resqrexlemgt0  11660  resqrexlemoverl  11661  resqrexlemglsq  11662  climi  11927  climcn1  11948  serf0  11992  fsum3cvg  12019  summodclem2  12023  summodc  12024  fsum3  12028  isumz  12030  fsumf1o  12031  isumss  12032  fisumss  12033  isumss2  12034  fsum3cvg2  12035  fsum3cvg3  12037  fsum3ser  12038  fsumsplit  12048  fsumm1  12057  fsum1p  12059  fisumcom2  12079  fsumge1  12102  telfsumo  12107  telfsumo2  12108  fsumparts  12111  isumshft  12131  isum1p  12133  isumnn0nn  12134  isumrpcl  12135  cvgratnnlemnexp  12165  cvgratnnlemmn  12166  cvgratnnlemseq  12167  cvgratnnlemabsle  12168  cvgratnnlemfm  12170  cvgratnnlemrate  12171  cvgratnn  12172  cvgratz  12173  mertenslemi1  12176  mertenslem2  12177  mertensabs  12178  fproddccvg  12213  prodmodclem2a  12217  prodmodc  12219  zproddc  12220  fprodseq  12224  prod1dc  12227  fprodf1o  12229  prodssdc  12230  fprodssdc  12231  fprodm1  12239  fprod1p  12240  fprodcom2fi  12267  sinltxirr  12402  bezoutlemmain  12649  bezoutlemex  12652  bezoutlemzz  12653  bezoutlemmo  12657  bezoutlemle  12659  bezoutlemsup  12660  nnmindc  12685  nnminle  12686  uzwodc  12688  nninfctlemfo  12691  prmind2  12772  isprm5lem  12793  isprm5  12794  pcmpt2  12997  prmpwdvds  13008  ennnfonelemk  13101  ennnfonelemex  13115  ennnfonelemnn0  13123  ctinfomlemom  13128  ctiunctlemudc  13138  ssnnctlemct  13147  nninfdclemcl  13149  nninfdclemp1  13151  nninfdc  13154  prdsbasprj  13445  lidrideqd  13544  grpinvalem  13548  grpinva  13549  grpidd2  13704  mulgsubcl  13803  issubg4m  13860  ghmf1  13940  gsumfzmhm2  14011  lringuplu  14291  mplsubgfilemcl  14800  icnpimaex  15022  lmcvg  15028  lmff  15060  cnmpt11  15094  cnmpt21  15102  comet  15310  dedekindeulemuub  15428  dedekindeulemloc  15430  dedekindeulemlu  15432  dedekindeulemeu  15433  suplociccreex  15435  suplociccex  15436  dedekindicclemuub  15437  dedekindicclemloc  15439  dedekindicclemlu  15441  dedekindicclemeu  15442  dedekindicc  15444  ivthinclemlopn  15447  ivthinclemlr  15448  ivthinclemuopn  15449  ivthinclemur  15450  ivthinclemdisj  15451  ivthinclemloc  15452  ivthinc  15454  ivthdec  15455  ivthreinc  15456  dich0  15463  limcimolemlt  15475  limcimo  15476  cnplimclemr  15480  cnlimci  15484  cnmptlimc  15485  limccnpcntop  15486  limccoap  15489  dvcoapbr  15518  eflt  15586  sin0pilem2  15593  pilem3  15594  perfectlem2  15814  lgsval2lem  15829  lgsdirnn0  15866  lgsdinn0  15867  2sqlem10  15944  eupth2lem3fi  16417  2omap  16715  subctctexmid  16722  pw1nct  16725  exmidnotnotr  16727  exmidcon  16728  exmidpeirce  16729  nnsf  16731  nninfalllem1  16734  nninfsellemeqinf  16742  isomninnlem  16762  trilpolemlt1  16773  trirec0  16776  apdiff  16780  iswomninnlem  16782  ismkvnnlem  16785  redcwlpolemeq1  16787  redc0  16790  reap0  16791  cndcap  16792  dceqnconst  16793  dcapnconst  16794  nconstwlpolem0  16796  nconstwlpolem  16798  neap0mkv  16802  ltlenmkv  16803