Theorem rspcdva 2912

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 2903	. 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 1395   e. wcel 2200   A.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 2801

This theorem is referenced by:  frirrg  4441  wetriext  4669  tfisi  4679  omsinds  4714  suppssov1  6215  caofref  6243  caofinvl  6244  caofdig  6252  oprssdmm  6317  tfrlem1  6454  tfrlem5  6460  tfr1onlemsucfn  6486  tfr1onlemsucaccv  6487  tfr1onlembxssdm  6489  tfr1onlembfn  6490  tfr1onlemaccex  6494  tfr1onlemres  6495  tfrcllemsucfn  6499  tfrcllemsucaccv  6500  tfrcllembxssdm  6502  tfrcllembfn  6503  tfrcllemaccex  6507  tfrcllemres  6508  tfrcl  6510  rdgon  6532  frecabcl  6545  pw2f1odclem  6995  undifdcss  7085  ctssdclemn0  7277  ctssdc  7280  nninfninc  7290  nnnninfeq  7295  nnnninfeq2  7296  enomnilem  7305  fodju0  7314  fodjuomnilemres  7315  ismkvnex  7322  fodjumkvlemres  7326  enmkvlem  7328  enwomnilem  7336  nninfdcinf  7338  nninfwlporlem  7340  nninfwlpoimlemdc  7344  nninfinfwlpolem  7345  exmidaclem  7390  exmidontriimlem4  7406  netap  7440  exmidapne  7446  cc2lem  7452  cc3  7454  prltlu  7674  cauappcvgprlemm  7832  caucvgprlemm  7855  caucvgprprlemml  7881  suplocexprlemmu  7905  suplocexprlemdisj  7907  suplocexprlemloc  7908  suplocexprlemub  7910  caucvgsrlemgt1  7982  caucvgsr  7989  suplocsrlemb  7993  suplocsrlempr  7994  suplocsrlem  7995  axcaucvglemcau  8085  axcaucvglemres  8086  axpre-suploclemres  8088  irrmulap  9843  suprzubdc  10456  nninfdcex  10457  zsupssdc  10458  exbtwnzlemstep  10467  apbtwnz  10494  frecuzrdgsuc  10636  frecuzrdgg  10638  frecuzrdgsuctlem  10645  uzsinds  10666  iseqovex  10680  seq3val  10682  seqvalcd  10683  seq3-1  10684  seqf  10686  seq3p1  10687  seqovcd  10689  seqp1cd  10692  seq3clss  10693  seq3fveq2  10697  seqfveq2g  10699  seqfveqg  10700  seq3fveq  10701  seq3feq  10702  seq3shft2  10703  seqshft2g  10704  monoord  10707  monoord2  10708  ser3mono  10709  seq3split  10710  seqsplitg  10711  seq3caopr3  10713  seqcaopr3g  10714  iseqf1olemkle  10719  iseqf1olemklt  10720  iseqf1olemjpcl  10730  iseqf1olemqpcl  10731  iseqf1olemfvp  10732  seq3f1olemqsumkj  10733  seq3f1olemqsum  10735  seq3f1oleml  10738  seq3f1o  10739  seqf1og  10743  seq3id3  10746  seq3id  10747  seq3id2  10748  seq3homo  10749  seq3z  10750  seqhomog  10752  seqfeq4g  10753  ser3ge0  10758  nn0ltexp2  10931  zfz1isolemiso  11061  wrdind  11254  seq3shft  11349  cvg1nlemcau  11495  cvg1nlemres  11496  recvguniq  11506  resqrexlemgt0  11531  resqrexlemoverl  11532  resqrexlemglsq  11533  climi  11798  climcn1  11819  serf0  11863  fsum3cvg  11889  summodclem2  11893  summodc  11894  fsum3  11898  isumz  11900  fsumf1o  11901  isumss  11902  fisumss  11903  isumss2  11904  fsum3cvg2  11905  fsum3cvg3  11907  fsum3ser  11908  fsumsplit  11918  fsumm1  11927  fsum1p  11929  fisumcom2  11949  fsumge1  11972  telfsumo  11977  telfsumo2  11978  fsumparts  11981  isumshft  12001  isum1p  12003  isumnn0nn  12004  isumrpcl  12005  cvgratnnlemnexp  12035  cvgratnnlemmn  12036  cvgratnnlemseq  12037  cvgratnnlemabsle  12038  cvgratnnlemfm  12040  cvgratnnlemrate  12041  cvgratnn  12042  cvgratz  12043  mertenslemi1  12046  mertenslem2  12047  mertensabs  12048  fproddccvg  12083  prodmodclem2a  12087  prodmodc  12089  zproddc  12090  fprodseq  12094  prod1dc  12097  fprodf1o  12099  prodssdc  12100  fprodssdc  12101  fprodm1  12109  fprod1p  12110  fprodcom2fi  12137  sinltxirr  12272  bezoutlemmain  12519  bezoutlemex  12522  bezoutlemzz  12523  bezoutlemmo  12527  bezoutlemle  12529  bezoutlemsup  12530  nnmindc  12555  nnminle  12556  uzwodc  12558  nninfctlemfo  12561  prmind2  12642  isprm5lem  12663  isprm5  12664  pcmpt2  12867  prmpwdvds  12878  ennnfonelemk  12971  ennnfonelemex  12985  ennnfonelemnn0  12993  ctinfomlemom  12998  ctiunctlemudc  13008  ssnnctlemct  13017  nninfdclemcl  13019  nninfdclemp1  13021  nninfdc  13024  prdsbasprj  13315  lidrideqd  13414  grpinvalem  13418  grpinva  13419  grpidd2  13574  mulgsubcl  13673  issubg4m  13730  ghmf1  13810  gsumfzmhm2  13881  lringuplu  14160  mplsubgfilemcl  14663  icnpimaex  14885  lmcvg  14891  lmff  14923  cnmpt11  14957  cnmpt21  14965  comet  15173  dedekindeulemuub  15291  dedekindeulemloc  15293  dedekindeulemlu  15295  dedekindeulemeu  15296  suplociccreex  15298  suplociccex  15299  dedekindicclemuub  15300  dedekindicclemloc  15302  dedekindicclemlu  15304  dedekindicclemeu  15305  dedekindicc  15307  ivthinclemlopn  15310  ivthinclemlr  15311  ivthinclemuopn  15312  ivthinclemur  15313  ivthinclemdisj  15314  ivthinclemloc  15315  ivthinc  15317  ivthdec  15318  ivthreinc  15319  dich0  15326  limcimolemlt  15338  limcimo  15339  cnplimclemr  15343  cnlimci  15347  cnmptlimc  15348  limccnpcntop  15349  limccoap  15352  dvcoapbr  15381  eflt  15449  sin0pilem2  15456  pilem3  15457  perfectlem2  15674  lgsval2lem  15689  lgsdirnn0  15726  lgsdinn0  15727  2sqlem10  15804  2omap  16359  subctctexmid  16366  pw1nct  16369  nnsf  16371  nninfalllem1  16374  nninfsellemeqinf  16382  isomninnlem  16398  trilpolemlt1  16409  trirec0  16412  apdiff  16416  iswomninnlem  16417  ismkvnnlem  16420  redcwlpolemeq1  16422  redc0  16425  reap0  16426  cndcap  16427  dceqnconst  16428  dcapnconst  16429  nconstwlpolem0  16431  nconstwlpolem  16433  neap0mkv  16437  ltlenmkv  16438