Theorem rspcdva 2873

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 2864	. 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 1364   e. wcel 2167   A.wral 2475

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-v 2765

This theorem is referenced by:  frirrg  4385  wetriext  4613  tfisi  4623  omsinds  4658  suppssov1  6132  caofref  6159  caofinvl  6160  caofdig  6164  oprssdmm  6229  tfrlem1  6366  tfrlem5  6372  tfr1onlemsucfn  6398  tfr1onlemsucaccv  6399  tfr1onlembxssdm  6401  tfr1onlembfn  6402  tfr1onlemaccex  6406  tfr1onlemres  6407  tfrcllemsucfn  6411  tfrcllemsucaccv  6412  tfrcllembxssdm  6414  tfrcllembfn  6415  tfrcllemaccex  6419  tfrcllemres  6420  tfrcl  6422  rdgon  6444  frecabcl  6457  pw2f1odclem  6895  undifdcss  6984  ctssdclemn0  7176  ctssdc  7179  nninfninc  7189  nnnninfeq  7194  nnnninfeq2  7195  enomnilem  7204  fodju0  7213  fodjuomnilemres  7214  ismkvnex  7221  fodjumkvlemres  7225  enmkvlem  7227  enwomnilem  7235  nninfdcinf  7237  nninfwlporlem  7239  nninfwlpoimlemdc  7243  exmidaclem  7275  exmidontriimlem4  7291  netap  7321  exmidapne  7327  cc2lem  7333  cc3  7335  prltlu  7554  cauappcvgprlemm  7712  caucvgprlemm  7735  caucvgprprlemml  7761  suplocexprlemmu  7785  suplocexprlemdisj  7787  suplocexprlemloc  7788  suplocexprlemub  7790  caucvgsrlemgt1  7862  caucvgsr  7869  suplocsrlemb  7873  suplocsrlempr  7874  suplocsrlem  7875  axcaucvglemcau  7965  axcaucvglemres  7966  axpre-suploclemres  7968  irrmulap  9722  suprzubdc  10326  nninfdcex  10327  zsupssdc  10328  exbtwnzlemstep  10337  apbtwnz  10364  frecuzrdgsuc  10506  frecuzrdgg  10508  frecuzrdgsuctlem  10515  uzsinds  10536  iseqovex  10550  seq3val  10552  seqvalcd  10553  seq3-1  10554  seqf  10556  seq3p1  10557  seqovcd  10559  seqp1cd  10562  seq3clss  10563  seq3fveq2  10567  seqfveq2g  10569  seqfveqg  10570  seq3fveq  10571  seq3feq  10572  seq3shft2  10573  seqshft2g  10574  monoord  10577  monoord2  10578  ser3mono  10579  seq3split  10580  seqsplitg  10581  seq3caopr3  10583  seqcaopr3g  10584  iseqf1olemkle  10589  iseqf1olemklt  10590  iseqf1olemjpcl  10600  iseqf1olemqpcl  10601  iseqf1olemfvp  10602  seq3f1olemqsumkj  10603  seq3f1olemqsum  10605  seq3f1oleml  10608  seq3f1o  10609  seqf1og  10613  seq3id3  10616  seq3id  10617  seq3id2  10618  seq3homo  10619  seq3z  10620  seqhomog  10622  seqfeq4g  10623  ser3ge0  10628  nn0ltexp2  10801  zfz1isolemiso  10931  seq3shft  11003  cvg1nlemcau  11149  cvg1nlemres  11150  recvguniq  11160  resqrexlemgt0  11185  resqrexlemoverl  11186  resqrexlemglsq  11187  climi  11452  climcn1  11473  serf0  11517  fsum3cvg  11543  summodclem2  11547  summodc  11548  fsum3  11552  isumz  11554  fsumf1o  11555  isumss  11556  fisumss  11557  isumss2  11558  fsum3cvg2  11559  fsum3cvg3  11561  fsum3ser  11562  fsumsplit  11572  fsumm1  11581  fsum1p  11583  fisumcom2  11603  fsumge1  11626  telfsumo  11631  telfsumo2  11632  fsumparts  11635  isumshft  11655  isum1p  11657  isumnn0nn  11658  isumrpcl  11659  cvgratnnlemnexp  11689  cvgratnnlemmn  11690  cvgratnnlemseq  11691  cvgratnnlemabsle  11692  cvgratnnlemfm  11694  cvgratnnlemrate  11695  cvgratnn  11696  cvgratz  11697  mertenslemi1  11700  mertenslem2  11701  mertensabs  11702  fproddccvg  11737  prodmodclem2a  11741  prodmodc  11743  zproddc  11744  fprodseq  11748  prod1dc  11751  fprodf1o  11753  prodssdc  11754  fprodssdc  11755  fprodm1  11763  fprod1p  11764  fprodcom2fi  11791  sinltxirr  11926  bezoutlemmain  12165  bezoutlemex  12168  bezoutlemzz  12169  bezoutlemmo  12173  bezoutlemle  12175  bezoutlemsup  12176  nnmindc  12201  nnminle  12202  uzwodc  12204  nninfctlemfo  12207  prmind2  12288  isprm5lem  12309  isprm5  12310  pcmpt2  12513  prmpwdvds  12524  ennnfonelemk  12617  ennnfonelemex  12631  ennnfonelemnn0  12639  ctinfomlemom  12644  ctiunctlemudc  12654  ssnnctlemct  12663  nninfdclemcl  12665  nninfdclemp1  12667  nninfdc  12670  lidrideqd  13024  grpinvalem  13028  grpinva  13029  grpidd2  13173  mulgsubcl  13266  issubg4m  13323  ghmf1  13403  gsumfzmhm2  13474  lringuplu  13752  icnpimaex  14447  lmcvg  14453  lmff  14485  cnmpt11  14519  cnmpt21  14527  comet  14735  dedekindeulemuub  14853  dedekindeulemloc  14855  dedekindeulemlu  14857  dedekindeulemeu  14858  suplociccreex  14860  suplociccex  14861  dedekindicclemuub  14862  dedekindicclemloc  14864  dedekindicclemlu  14866  dedekindicclemeu  14867  dedekindicc  14869  ivthinclemlopn  14872  ivthinclemlr  14873  ivthinclemuopn  14874  ivthinclemur  14875  ivthinclemdisj  14876  ivthinclemloc  14877  ivthinc  14879  ivthdec  14880  ivthreinc  14881  dich0  14888  limcimolemlt  14900  limcimo  14901  cnplimclemr  14905  cnlimci  14909  cnmptlimc  14910  limccnpcntop  14911  limccoap  14914  dvcoapbr  14943  eflt  15011  sin0pilem2  15018  pilem3  15019  perfectlem2  15236  lgsval2lem  15251  lgsdirnn0  15288  lgsdinn0  15289  2sqlem10  15366  subctctexmid  15645  pw1nct  15647  nnsf  15649  nninfalllem1  15652  nninfsellemeqinf  15660  isomninnlem  15674  trilpolemlt1  15685  trirec0  15688  apdiff  15692  iswomninnlem  15693  ismkvnnlem  15696  redcwlpolemeq1  15698  redc0  15701  reap0  15702  cndcap  15703  dceqnconst  15704  dcapnconst  15705  nconstwlpolem0  15707  nconstwlpolem  15709  neap0mkv  15713  ltlenmkv  15714