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  4386  wetriext  4614  tfisi  4624  omsinds  4659  suppssov1  6136  caofref  6164  caofinvl  6165  caofdig  6173  oprssdmm  6238  tfrlem1  6375  tfrlem5  6381  tfr1onlemsucfn  6407  tfr1onlemsucaccv  6408  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfr1onlemaccex  6415  tfr1onlemres  6416  tfrcllemsucfn  6420  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllembfn  6424  tfrcllemaccex  6428  tfrcllemres  6429  tfrcl  6431  rdgon  6453  frecabcl  6466  pw2f1odclem  6904  undifdcss  6993  ctssdclemn0  7185  ctssdc  7188  nninfninc  7198  nnnninfeq  7203  nnnninfeq2  7204  enomnilem  7213  fodju0  7222  fodjuomnilemres  7223  ismkvnex  7230  fodjumkvlemres  7234  enmkvlem  7236  enwomnilem  7244  nninfdcinf  7246  nninfwlporlem  7248  nninfwlpoimlemdc  7252  exmidaclem  7291  exmidontriimlem4  7307  netap  7337  exmidapne  7343  cc2lem  7349  cc3  7351  prltlu  7571  cauappcvgprlemm  7729  caucvgprlemm  7752  caucvgprprlemml  7778  suplocexprlemmu  7802  suplocexprlemdisj  7804  suplocexprlemloc  7805  suplocexprlemub  7807  caucvgsrlemgt1  7879  caucvgsr  7886  suplocsrlemb  7890  suplocsrlempr  7891  suplocsrlem  7892  axcaucvglemcau  7982  axcaucvglemres  7983  axpre-suploclemres  7985  irrmulap  9739  suprzubdc  10343  nninfdcex  10344  zsupssdc  10345  exbtwnzlemstep  10354  apbtwnz  10381  frecuzrdgsuc  10523  frecuzrdgg  10525  frecuzrdgsuctlem  10532  uzsinds  10553  iseqovex  10567  seq3val  10569  seqvalcd  10570  seq3-1  10571  seqf  10573  seq3p1  10574  seqovcd  10576  seqp1cd  10579  seq3clss  10580  seq3fveq2  10584  seqfveq2g  10586  seqfveqg  10587  seq3fveq  10588  seq3feq  10589  seq3shft2  10590  seqshft2g  10591  monoord  10594  monoord2  10595  ser3mono  10596  seq3split  10597  seqsplitg  10598  seq3caopr3  10600  seqcaopr3g  10601  iseqf1olemkle  10606  iseqf1olemklt  10607  iseqf1olemjpcl  10617  iseqf1olemqpcl  10618  iseqf1olemfvp  10619  seq3f1olemqsumkj  10620  seq3f1olemqsum  10622  seq3f1oleml  10625  seq3f1o  10626  seqf1og  10630  seq3id3  10633  seq3id  10634  seq3id2  10635  seq3homo  10636  seq3z  10637  seqhomog  10639  seqfeq4g  10640  ser3ge0  10645  nn0ltexp2  10818  zfz1isolemiso  10948  seq3shft  11020  cvg1nlemcau  11166  cvg1nlemres  11167  recvguniq  11177  resqrexlemgt0  11202  resqrexlemoverl  11203  resqrexlemglsq  11204  climi  11469  climcn1  11490  serf0  11534  fsum3cvg  11560  summodclem2  11564  summodc  11565  fsum3  11569  isumz  11571  fsumf1o  11572  isumss  11573  fisumss  11574  isumss2  11575  fsum3cvg2  11576  fsum3cvg3  11578  fsum3ser  11579  fsumsplit  11589  fsumm1  11598  fsum1p  11600  fisumcom2  11620  fsumge1  11643  telfsumo  11648  telfsumo2  11649  fsumparts  11652  isumshft  11672  isum1p  11674  isumnn0nn  11675  isumrpcl  11676  cvgratnnlemnexp  11706  cvgratnnlemmn  11707  cvgratnnlemseq  11708  cvgratnnlemabsle  11709  cvgratnnlemfm  11711  cvgratnnlemrate  11712  cvgratnn  11713  cvgratz  11714  mertenslemi1  11717  mertenslem2  11718  mertensabs  11719  fproddccvg  11754  prodmodclem2a  11758  prodmodc  11760  zproddc  11761  fprodseq  11765  prod1dc  11768  fprodf1o  11770  prodssdc  11771  fprodssdc  11772  fprodm1  11780  fprod1p  11781  fprodcom2fi  11808  sinltxirr  11943  bezoutlemmain  12190  bezoutlemex  12193  bezoutlemzz  12194  bezoutlemmo  12198  bezoutlemle  12200  bezoutlemsup  12201  nnmindc  12226  nnminle  12227  uzwodc  12229  nninfctlemfo  12232  prmind2  12313  isprm5lem  12334  isprm5  12335  pcmpt2  12538  prmpwdvds  12549  ennnfonelemk  12642  ennnfonelemex  12656  ennnfonelemnn0  12664  ctinfomlemom  12669  ctiunctlemudc  12679  ssnnctlemct  12688  nninfdclemcl  12690  nninfdclemp1  12692  nninfdc  12695  prdsbasprj  12984  lidrideqd  13083  grpinvalem  13087  grpinva  13088  grpidd2  13243  mulgsubcl  13342  issubg4m  13399  ghmf1  13479  gsumfzmhm2  13550  lringuplu  13828  icnpimaex  14531  lmcvg  14537  lmff  14569  cnmpt11  14603  cnmpt21  14611  comet  14819  dedekindeulemuub  14937  dedekindeulemloc  14939  dedekindeulemlu  14941  dedekindeulemeu  14942  suplociccreex  14944  suplociccex  14945  dedekindicclemuub  14946  dedekindicclemloc  14948  dedekindicclemlu  14950  dedekindicclemeu  14951  dedekindicc  14953  ivthinclemlopn  14956  ivthinclemlr  14957  ivthinclemuopn  14958  ivthinclemur  14959  ivthinclemdisj  14960  ivthinclemloc  14961  ivthinc  14963  ivthdec  14964  ivthreinc  14965  dich0  14972  limcimolemlt  14984  limcimo  14985  cnplimclemr  14989  cnlimci  14993  cnmptlimc  14994  limccnpcntop  14995  limccoap  14998  dvcoapbr  15027  eflt  15095  sin0pilem2  15102  pilem3  15103  perfectlem2  15320  lgsval2lem  15335  lgsdirnn0  15372  lgsdinn0  15373  2sqlem10  15450  2omap  15726  subctctexmid  15731  pw1nct  15734  nnsf  15736  nninfalllem1  15739  nninfsellemeqinf  15747  isomninnlem  15761  trilpolemlt1  15772  trirec0  15775  apdiff  15779  iswomninnlem  15780  ismkvnnlem  15783  redcwlpolemeq1  15785  redc0  15788  reap0  15789  cndcap  15790  dceqnconst  15791  dcapnconst  15792  nconstwlpolem0  15794  nconstwlpolem  15796  neap0mkv  15800  ltlenmkv  15801