Theorem rspcdva 2834

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 2825	. 2 |- ( C e. A -> ( A. x e. A ps -> ch ) )
5	1, 2, 4	sylc 62	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1343   e. wcel 2136   A.wral 2443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-ral 2448  df-v 2727

This theorem is referenced by:  frirrg  4327  wetriext  4553  tfisi  4563  omsinds  4598  grprinvlem  6032  grprinvd  6033  suppssov1  6046  caofref  6070  caofinvl  6071  oprssdmm  6136  tfrlem1  6272  tfrlem5  6278  tfr1onlemsucfn  6304  tfr1onlemsucaccv  6305  tfr1onlembxssdm  6307  tfr1onlembfn  6308  tfr1onlemaccex  6312  tfr1onlemres  6313  tfrcllemsucfn  6317  tfrcllemsucaccv  6318  tfrcllembxssdm  6320  tfrcllembfn  6321  tfrcllemaccex  6325  tfrcllemres  6326  tfrcl  6328  rdgon  6350  frecabcl  6363  undifdcss  6884  ctssdclemn0  7071  ctssdc  7074  nnnninfeq  7088  nnnninfeq2  7089  enomnilem  7098  fodju0  7107  fodjuomnilemres  7108  ismkvnex  7115  fodjumkvlemres  7119  enmkvlem  7121  enwomnilem  7129  exmidaclem  7160  exmidontriimlem4  7176  cc2lem  7203  cc3  7205  prltlu  7424  cauappcvgprlemm  7582  caucvgprlemm  7605  caucvgprprlemml  7631  suplocexprlemmu  7655  suplocexprlemdisj  7657  suplocexprlemloc  7658  suplocexprlemub  7660  caucvgsrlemgt1  7732  caucvgsr  7739  suplocsrlemb  7743  suplocsrlempr  7744  suplocsrlem  7745  axcaucvglemcau  7835  axcaucvglemres  7836  axpre-suploclemres  7838  exbtwnzlemstep  10179  apbtwnz  10205  frecuzrdgsuc  10345  frecuzrdgg  10347  frecuzrdgsuctlem  10354  uzsinds  10373  iseqovex  10387  seq3val  10389  seqvalcd  10390  seq3-1  10391  seqf  10392  seq3p1  10393  seqovcd  10394  seqp1cd  10397  seq3clss  10398  seq3fveq2  10400  seq3fveq  10402  seq3feq  10403  seq3shft2  10404  monoord  10407  monoord2  10408  ser3mono  10409  seq3split  10410  seq3caopr3  10412  iseqf1olemkle  10415  iseqf1olemklt  10416  iseqf1olemjpcl  10426  iseqf1olemqpcl  10427  iseqf1olemfvp  10428  seq3f1olemqsumkj  10429  seq3f1olemqsum  10431  seq3f1oleml  10434  seq3f1o  10435  seq3id3  10438  seq3id  10439  seq3id2  10440  seq3homo  10441  seq3z  10442  ser3ge0  10448  nn0ltexp2  10619  zfz1isolemiso  10748  seq3shft  10776  cvg1nlemcau  10922  cvg1nlemres  10923  recvguniq  10933  resqrexlemgt0  10958  resqrexlemoverl  10959  resqrexlemglsq  10960  climi  11224  climcn1  11245  serf0  11289  fsum3cvg  11315  summodclem2  11319  summodc  11320  fsum3  11324  isumz  11326  fsumf1o  11327  isumss  11328  fisumss  11329  isumss2  11330  fsum3cvg2  11331  fsum3cvg3  11333  fsum3ser  11334  fsumsplit  11344  fsumm1  11353  fsum1p  11355  fisumcom2  11375  fsumge1  11398  telfsumo  11403  telfsumo2  11404  fsumparts  11407  isumshft  11427  isum1p  11429  isumnn0nn  11430  isumrpcl  11431  cvgratnnlemnexp  11461  cvgratnnlemmn  11462  cvgratnnlemseq  11463  cvgratnnlemabsle  11464  cvgratnnlemfm  11466  cvgratnnlemrate  11467  cvgratnn  11468  cvgratz  11469  mertenslemi1  11472  mertenslem2  11473  mertensabs  11474  fproddccvg  11509  prodmodclem2a  11513  prodmodc  11515  zproddc  11516  fprodseq  11520  prod1dc  11523  fprodf1o  11525  prodssdc  11526  fprodssdc  11527  fprodm1  11535  fprod1p  11536  fprodcom2fi  11563  suprzubdc  11881  nninfdcex  11882  zsupssdc  11883  bezoutlemmain  11927  bezoutlemex  11930  bezoutlemzz  11931  bezoutlemmo  11935  bezoutlemle  11937  bezoutlemsup  11938  nnmindc  11963  nnminle  11964  uzwodc  11966  prmind2  12048  isprm5lem  12069  isprm5  12070  pcmpt2  12270  prmpwdvds  12281  ennnfonelemk  12329  ennnfonelemex  12343  ennnfonelemnn0  12351  ctinfomlemom  12356  ctiunctlemudc  12366  ssnnctlemct  12375  nninfdclemcl  12377  nninfdclemp1  12379  nninfdc  12382  icnpimaex  12811  lmcvg  12817  lmff  12849  cnmpt11  12883  cnmpt21  12891  comet  13099  dedekindeulemuub  13195  dedekindeulemloc  13197  dedekindeulemlu  13199  dedekindeulemeu  13200  suplociccreex  13202  suplociccex  13203  dedekindicclemuub  13204  dedekindicclemloc  13206  dedekindicclemlu  13208  dedekindicclemeu  13209  dedekindicc  13211  ivthinclemlopn  13214  ivthinclemlr  13215  ivthinclemuopn  13216  ivthinclemur  13217  ivthinclemdisj  13218  ivthinclemloc  13219  ivthinc  13221  ivthdec  13222  limcimolemlt  13233  limcimo  13234  cnplimclemr  13238  cnlimci  13242  cnmptlimc  13243  limccnpcntop  13244  limccoap  13247  dvcoapbr  13271  eflt  13296  sin0pilem2  13303  pilem3  13304  lgsval2lem  13511  lgsdirnn0  13548  lgsdinn0  13549  2sqlem10  13561  subctctexmid  13841  pw1nct  13843  nnsf  13845  nninfalllem1  13848  nninfsellemeqinf  13856  isomninnlem  13869  trilpolemlt1  13880  trirec0  13883  apdiff  13887  iswomninnlem  13888  ismkvnnlem  13891  redcwlpolemeq1  13893  redc0  13896  reap0  13897  dceqnconst  13898  dcapnconst  13899  nconstwlpolem0  13901  nconstwlpolem  13903