Theorem rspcdva 2882

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 2873	. 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 1373   e. wcel 2176   A.wral 2484

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-v 2774

This theorem is referenced by:  frirrg  4398  wetriext  4626  tfisi  4636  omsinds  4671  suppssov1  6157  caofref  6185  caofinvl  6186  caofdig  6194  oprssdmm  6259  tfrlem1  6396  tfrlem5  6402  tfr1onlemsucfn  6428  tfr1onlemsucaccv  6429  tfr1onlembxssdm  6431  tfr1onlembfn  6432  tfr1onlemaccex  6436  tfr1onlemres  6437  tfrcllemsucfn  6441  tfrcllemsucaccv  6442  tfrcllembxssdm  6444  tfrcllembfn  6445  tfrcllemaccex  6449  tfrcllemres  6450  tfrcl  6452  rdgon  6474  frecabcl  6487  pw2f1odclem  6933  undifdcss  7022  ctssdclemn0  7214  ctssdc  7217  nninfninc  7227  nnnninfeq  7232  nnnninfeq2  7233  enomnilem  7242  fodju0  7251  fodjuomnilemres  7252  ismkvnex  7259  fodjumkvlemres  7263  enmkvlem  7265  enwomnilem  7273  nninfdcinf  7275  nninfwlporlem  7277  nninfwlpoimlemdc  7281  nninfinfwlpolem  7282  exmidaclem  7322  exmidontriimlem4  7338  netap  7368  exmidapne  7374  cc2lem  7380  cc3  7382  prltlu  7602  cauappcvgprlemm  7760  caucvgprlemm  7783  caucvgprprlemml  7809  suplocexprlemmu  7833  suplocexprlemdisj  7835  suplocexprlemloc  7836  suplocexprlemub  7838  caucvgsrlemgt1  7910  caucvgsr  7917  suplocsrlemb  7921  suplocsrlempr  7922  suplocsrlem  7923  axcaucvglemcau  8013  axcaucvglemres  8014  axpre-suploclemres  8016  irrmulap  9771  suprzubdc  10381  nninfdcex  10382  zsupssdc  10383  exbtwnzlemstep  10392  apbtwnz  10419  frecuzrdgsuc  10561  frecuzrdgg  10563  frecuzrdgsuctlem  10570  uzsinds  10591  iseqovex  10605  seq3val  10607  seqvalcd  10608  seq3-1  10609  seqf  10611  seq3p1  10612  seqovcd  10614  seqp1cd  10617  seq3clss  10618  seq3fveq2  10622  seqfveq2g  10624  seqfveqg  10625  seq3fveq  10626  seq3feq  10627  seq3shft2  10628  seqshft2g  10629  monoord  10632  monoord2  10633  ser3mono  10634  seq3split  10635  seqsplitg  10636  seq3caopr3  10638  seqcaopr3g  10639  iseqf1olemkle  10644  iseqf1olemklt  10645  iseqf1olemjpcl  10655  iseqf1olemqpcl  10656  iseqf1olemfvp  10657  seq3f1olemqsumkj  10658  seq3f1olemqsum  10660  seq3f1oleml  10663  seq3f1o  10664  seqf1og  10668  seq3id3  10671  seq3id  10672  seq3id2  10673  seq3homo  10674  seq3z  10675  seqhomog  10677  seqfeq4g  10678  ser3ge0  10683  nn0ltexp2  10856  zfz1isolemiso  10986  seq3shft  11182  cvg1nlemcau  11328  cvg1nlemres  11329  recvguniq  11339  resqrexlemgt0  11364  resqrexlemoverl  11365  resqrexlemglsq  11366  climi  11631  climcn1  11652  serf0  11696  fsum3cvg  11722  summodclem2  11726  summodc  11727  fsum3  11731  isumz  11733  fsumf1o  11734  isumss  11735  fisumss  11736  isumss2  11737  fsum3cvg2  11738  fsum3cvg3  11740  fsum3ser  11741  fsumsplit  11751  fsumm1  11760  fsum1p  11762  fisumcom2  11782  fsumge1  11805  telfsumo  11810  telfsumo2  11811  fsumparts  11814  isumshft  11834  isum1p  11836  isumnn0nn  11837  isumrpcl  11838  cvgratnnlemnexp  11868  cvgratnnlemmn  11869  cvgratnnlemseq  11870  cvgratnnlemabsle  11871  cvgratnnlemfm  11873  cvgratnnlemrate  11874  cvgratnn  11875  cvgratz  11876  mertenslemi1  11879  mertenslem2  11880  mertensabs  11881  fproddccvg  11916  prodmodclem2a  11920  prodmodc  11922  zproddc  11923  fprodseq  11927  prod1dc  11930  fprodf1o  11932  prodssdc  11933  fprodssdc  11934  fprodm1  11942  fprod1p  11943  fprodcom2fi  11970  sinltxirr  12105  bezoutlemmain  12352  bezoutlemex  12355  bezoutlemzz  12356  bezoutlemmo  12360  bezoutlemle  12362  bezoutlemsup  12363  nnmindc  12388  nnminle  12389  uzwodc  12391  nninfctlemfo  12394  prmind2  12475  isprm5lem  12496  isprm5  12497  pcmpt2  12700  prmpwdvds  12711  ennnfonelemk  12804  ennnfonelemex  12818  ennnfonelemnn0  12826  ctinfomlemom  12831  ctiunctlemudc  12841  ssnnctlemct  12850  nninfdclemcl  12852  nninfdclemp1  12854  nninfdc  12857  prdsbasprj  13147  lidrideqd  13246  grpinvalem  13250  grpinva  13251  grpidd2  13406  mulgsubcl  13505  issubg4m  13562  ghmf1  13642  gsumfzmhm2  13713  lringuplu  13991  mplsubgfilemcl  14494  icnpimaex  14716  lmcvg  14722  lmff  14754  cnmpt11  14788  cnmpt21  14796  comet  15004  dedekindeulemuub  15122  dedekindeulemloc  15124  dedekindeulemlu  15126  dedekindeulemeu  15127  suplociccreex  15129  suplociccex  15130  dedekindicclemuub  15131  dedekindicclemloc  15133  dedekindicclemlu  15135  dedekindicclemeu  15136  dedekindicc  15138  ivthinclemlopn  15141  ivthinclemlr  15142  ivthinclemuopn  15143  ivthinclemur  15144  ivthinclemdisj  15145  ivthinclemloc  15146  ivthinc  15148  ivthdec  15149  ivthreinc  15150  dich0  15157  limcimolemlt  15169  limcimo  15170  cnplimclemr  15174  cnlimci  15178  cnmptlimc  15179  limccnpcntop  15180  limccoap  15183  dvcoapbr  15212  eflt  15280  sin0pilem2  15287  pilem3  15288  perfectlem2  15505  lgsval2lem  15520  lgsdirnn0  15557  lgsdinn0  15558  2sqlem10  15635  2omap  15969  subctctexmid  15974  pw1nct  15977  nnsf  15979  nninfalllem1  15982  nninfsellemeqinf  15990  isomninnlem  16006  trilpolemlt1  16017  trirec0  16020  apdiff  16024  iswomninnlem  16025  ismkvnnlem  16028  redcwlpolemeq1  16030  redc0  16033  reap0  16034  cndcap  16035  dceqnconst  16036  dcapnconst  16037  nconstwlpolem0  16039  nconstwlpolem  16041  neap0mkv  16045  ltlenmkv  16046