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  6221  caofref  6249  caofinvl  6250  caofdig  6258  oprssdmm  6323  tfrlem1  6460  tfrlem5  6466  tfr1onlemsucfn  6492  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfr1onlemaccex  6500  tfr1onlemres  6501  tfrcllemsucfn  6505  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllembfn  6509  tfrcllemaccex  6513  tfrcllemres  6514  tfrcl  6516  rdgon  6538  frecabcl  6551  pw2f1odclem  7003  elssdc  7075  undifdcss  7096  ctssdclemn0  7288  ctssdc  7291  nninfninc  7301  nnnninfeq  7306  nnnninfeq2  7307  enomnilem  7316  fodju0  7325  fodjuomnilemres  7326  ismkvnex  7333  fodjumkvlemres  7337  enmkvlem  7339  enwomnilem  7347  nninfdcinf  7349  nninfwlporlem  7351  nninfwlpoimlemdc  7355  nninfinfwlpolem  7356  exmidaclem  7401  exmidontriimlem4  7417  netap  7451  exmidapne  7457  cc2lem  7463  cc3  7465  prltlu  7685  cauappcvgprlemm  7843  caucvgprlemm  7866  caucvgprprlemml  7892  suplocexprlemmu  7916  suplocexprlemdisj  7918  suplocexprlemloc  7919  suplocexprlemub  7921  caucvgsrlemgt1  7993  caucvgsr  8000  suplocsrlemb  8004  suplocsrlempr  8005  suplocsrlem  8006  axcaucvglemcau  8096  axcaucvglemres  8097  axpre-suploclemres  8099  irrmulap  9855  suprzubdc  10468  nninfdcex  10469  zsupssdc  10470  exbtwnzlemstep  10479  apbtwnz  10506  frecuzrdgsuc  10648  frecuzrdgg  10650  frecuzrdgsuctlem  10657  uzsinds  10678  iseqovex  10692  seq3val  10694  seqvalcd  10695  seq3-1  10696  seqf  10698  seq3p1  10699  seqovcd  10701  seqp1cd  10704  seq3clss  10705  seq3fveq2  10709  seqfveq2g  10711  seqfveqg  10712  seq3fveq  10713  seq3feq  10714  seq3shft2  10715  seqshft2g  10716  monoord  10719  monoord2  10720  ser3mono  10721  seq3split  10722  seqsplitg  10723  seq3caopr3  10725  seqcaopr3g  10726  iseqf1olemkle  10731  iseqf1olemklt  10732  iseqf1olemjpcl  10742  iseqf1olemqpcl  10743  iseqf1olemfvp  10744  seq3f1olemqsumkj  10745  seq3f1olemqsum  10747  seq3f1oleml  10750  seq3f1o  10751  seqf1og  10755  seq3id3  10758  seq3id  10759  seq3id2  10760  seq3homo  10761  seq3z  10762  seqhomog  10764  seqfeq4g  10765  ser3ge0  10770  nn0ltexp2  10943  zfz1isolemiso  11074  wrdind  11270  seq3shft  11365  cvg1nlemcau  11511  cvg1nlemres  11512  recvguniq  11522  resqrexlemgt0  11547  resqrexlemoverl  11548  resqrexlemglsq  11549  climi  11814  climcn1  11835  serf0  11879  fsum3cvg  11905  summodclem2  11909  summodc  11910  fsum3  11914  isumz  11916  fsumf1o  11917  isumss  11918  fisumss  11919  isumss2  11920  fsum3cvg2  11921  fsum3cvg3  11923  fsum3ser  11924  fsumsplit  11934  fsumm1  11943  fsum1p  11945  fisumcom2  11965  fsumge1  11988  telfsumo  11993  telfsumo2  11994  fsumparts  11997  isumshft  12017  isum1p  12019  isumnn0nn  12020  isumrpcl  12021  cvgratnnlemnexp  12051  cvgratnnlemmn  12052  cvgratnnlemseq  12053  cvgratnnlemabsle  12054  cvgratnnlemfm  12056  cvgratnnlemrate  12057  cvgratnn  12058  cvgratz  12059  mertenslemi1  12062  mertenslem2  12063  mertensabs  12064  fproddccvg  12099  prodmodclem2a  12103  prodmodc  12105  zproddc  12106  fprodseq  12110  prod1dc  12113  fprodf1o  12115  prodssdc  12116  fprodssdc  12117  fprodm1  12125  fprod1p  12126  fprodcom2fi  12153  sinltxirr  12288  bezoutlemmain  12535  bezoutlemex  12538  bezoutlemzz  12539  bezoutlemmo  12543  bezoutlemle  12545  bezoutlemsup  12546  nnmindc  12571  nnminle  12572  uzwodc  12574  nninfctlemfo  12577  prmind2  12658  isprm5lem  12679  isprm5  12680  pcmpt2  12883  prmpwdvds  12894  ennnfonelemk  12987  ennnfonelemex  13001  ennnfonelemnn0  13009  ctinfomlemom  13014  ctiunctlemudc  13024  ssnnctlemct  13033  nninfdclemcl  13035  nninfdclemp1  13037  nninfdc  13040  prdsbasprj  13331  lidrideqd  13430  grpinvalem  13434  grpinva  13435  grpidd2  13590  mulgsubcl  13689  issubg4m  13746  ghmf1  13826  gsumfzmhm2  13897  lringuplu  14176  mplsubgfilemcl  14679  icnpimaex  14901  lmcvg  14907  lmff  14939  cnmpt11  14973  cnmpt21  14981  comet  15189  dedekindeulemuub  15307  dedekindeulemloc  15309  dedekindeulemlu  15311  dedekindeulemeu  15312  suplociccreex  15314  suplociccex  15315  dedekindicclemuub  15316  dedekindicclemloc  15318  dedekindicclemlu  15320  dedekindicclemeu  15321  dedekindicc  15323  ivthinclemlopn  15326  ivthinclemlr  15327  ivthinclemuopn  15328  ivthinclemur  15329  ivthinclemdisj  15330  ivthinclemloc  15331  ivthinc  15333  ivthdec  15334  ivthreinc  15335  dich0  15342  limcimolemlt  15354  limcimo  15355  cnplimclemr  15359  cnlimci  15363  cnmptlimc  15364  limccnpcntop  15365  limccoap  15368  dvcoapbr  15397  eflt  15465  sin0pilem2  15472  pilem3  15473  perfectlem2  15690  lgsval2lem  15705  lgsdirnn0  15742  lgsdinn0  15743  2sqlem10  15820  2omap  16446  subctctexmid  16453  pw1nct  16456  nnsf  16459  nninfalllem1  16462  nninfsellemeqinf  16470  isomninnlem  16486  trilpolemlt1  16497  trirec0  16500  apdiff  16504  iswomninnlem  16505  ismkvnnlem  16508  redcwlpolemeq1  16510  redc0  16513  reap0  16514  cndcap  16515  dceqnconst  16516  dcapnconst  16517  nconstwlpolem0  16519  nconstwlpolem  16521  neap0mkv  16525  ltlenmkv  16526