Theorem rspcdva 2926

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 2917	. 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 1398   e. wcel 2203   A.wral 2520

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-v 2815

This theorem is referenced by:  frirrg  4471  wetriext  4699  tfisi  4709  omsinds  4744  suppssov1  6263  caofref  6291  caofinvl  6292  caofdig  6300  oprssdmm  6365  suppssdc  6460  suppssrst  6461  suppssrgst  6462  suppofss1dcl  6464  suppofss2dcl  6465  tfrlem1  6539  tfrlem5  6545  tfr1onlemsucfn  6571  tfr1onlemsucaccv  6572  tfr1onlembxssdm  6574  tfr1onlembfn  6575  tfr1onlemaccex  6579  tfr1onlemres  6580  tfrcllemsucfn  6584  tfrcllemsucaccv  6585  tfrcllembxssdm  6587  tfrcllembfn  6588  tfrcllemaccex  6592  tfrcllemres  6593  tfrcl  6595  rdgon  6617  frecabcl  6630  pw2f1odclem  7087  elssdc  7162  undifdcss  7183  2omap  7269  ctssdclemn0  7401  ctssdc  7404  nninfninc  7414  nnnninfeq  7419  nnnninfeq2  7420  enomnilem  7429  fodju0  7438  fodjuomnilemres  7439  ismkvnex  7446  fodjumkvlemres  7450  enmkvlem  7452  enwomnilem  7460  nninfdcinf  7462  nninfwlporlem  7464  nninfwlpoimlemdc  7468  nninfinfwlpolem  7469  exmidaclem  7515  exmidontriimlem4  7531  papirr  7560  papsym  7561  papcotr  7562  netap  7568  exmidapne  7574  cc2lem  7580  cc3  7582  prltlu  7802  cauappcvgprlemm  7960  caucvgprlemm  7983  caucvgprprlemml  8009  suplocexprlemmu  8033  suplocexprlemdisj  8035  suplocexprlemloc  8036  suplocexprlemub  8038  caucvgsrlemgt1  8110  caucvgsr  8117  suplocsrlemb  8121  suplocsrlempr  8122  suplocsrlem  8123  axcaucvglemcau  8213  axcaucvglemres  8214  axpre-suploclemres  8216  irrmulap  9980  suprzubdc  10596  nninfdcex  10597  zsupssdc  10598  exbtwnzlemstep  10607  apbtwnz  10634  frecuzrdgsuc  10776  frecuzrdgg  10778  frecuzrdgsuctlem  10785  uzsinds  10806  iseqovex  10820  seq3val  10822  seqvalcd  10823  seq3-1  10824  seqf  10826  seq3p1  10827  seqovcd  10829  seqp1cd  10832  seq3clss  10833  seq3fveq2  10837  seqfveq2g  10839  seqfveqg  10840  seq3fveq  10841  seq3feq  10842  seq3shft2  10843  seqshft2g  10844  monoord  10847  monoord2  10848  ser3mono  10849  seq3split  10850  seqsplitg  10851  seq3caopr3  10853  seqcaopr3g  10854  iseqf1olemkle  10859  iseqf1olemklt  10860  iseqf1olemjpcl  10870  iseqf1olemqpcl  10871  iseqf1olemfvp  10872  seq3f1olemqsumkj  10873  seq3f1olemqsum  10875  seq3f1oleml  10878  seq3f1o  10879  seqf1og  10883  seq3id3  10886  seq3id  10887  seq3id2  10888  seq3homo  10889  seq3z  10890  seqhomog  10892  seqfeq4g  10893  ser3ge0  10898  nn0ltexp2  11071  hashfibclem  11206  zfz1isolemiso  11211  wrdind  11414  seq3shft  11523  cvg1nlemcau  11669  cvg1nlemres  11670  recvguniq  11680  resqrexlemgt0  11705  resqrexlemoverl  11706  resqrexlemglsq  11707  climi  11972  climcn1  11993  serf0  12037  fsum3cvg  12064  summodclem2  12068  summodc  12069  fsum3  12073  isumz  12075  fsumf1o  12076  isumss  12077  fisumss  12078  isumss2  12079  fsum3cvg2  12080  fsum3cvg3  12082  fsum3ser  12083  fsumsplit  12093  fsumm1  12102  fsum1p  12104  fisumcom2  12124  fsumge1  12147  telfsumo  12152  telfsumo2  12153  fsumparts  12156  isumshft  12176  isum1p  12178  isumnn0nn  12179  isumrpcl  12180  cvgratnnlemnexp  12210  cvgratnnlemmn  12211  cvgratnnlemseq  12212  cvgratnnlemabsle  12213  cvgratnnlemfm  12215  cvgratnnlemrate  12216  cvgratnn  12217  cvgratz  12218  mertenslemi1  12221  mertenslem2  12222  mertensabs  12223  fproddccvg  12258  prodmodclem2a  12262  prodmodc  12264  zproddc  12265  fprodseq  12269  prod1dc  12272  fprodf1o  12274  prodssdc  12275  fprodssdc  12276  fprodm1  12284  fprod1p  12285  fprodcom2fi  12312  sinltxirr  12447  bezoutlemmain  12694  bezoutlemex  12697  bezoutlemzz  12698  bezoutlemmo  12702  bezoutlemle  12704  bezoutlemsup  12705  nnmindc  12730  nnminle  12731  uzwodc  12733  nninfctlemfo  12736  prmind2  12817  isprm5lem  12838  isprm5  12839  pcmpt2  13042  prmpwdvds  13053  ennnfonelemk  13151  ennnfonelemex  13165  ennnfonelemnn0  13173  ctinfomlemom  13178  ctiunctlemudc  13188  ssnnctlemct  13197  nninfdclemcl  13199  nninfdclemp1  13201  nninfdc  13204  prdsbasprj  13495  lidrideqd  13594  grpinvalem  13598  grpinva  13599  grpidd2  13754  mulgsubcl  13853  issubg4m  13910  ghmf1  13990  gsumfzmhm2  14061  lringuplu  14341  mplsubgfilemcl  14854  icnpimaex  15076  lmcvg  15082  lmff  15114  cnmpt11  15148  cnmpt21  15156  comet  15364  dedekindeulemuub  15482  dedekindeulemloc  15484  dedekindeulemlu  15486  dedekindeulemeu  15487  suplociccreex  15489  suplociccex  15490  dedekindicclemuub  15491  dedekindicclemloc  15493  dedekindicclemlu  15495  dedekindicclemeu  15496  dedekindicc  15498  ivthinclemlopn  15501  ivthinclemlr  15502  ivthinclemuopn  15503  ivthinclemur  15504  ivthinclemdisj  15505  ivthinclemloc  15506  ivthinc  15508  ivthdec  15509  ivthreinc  15510  dich0  15517  limcimolemlt  15529  limcimo  15530  cnplimclemr  15534  cnlimci  15538  cnmptlimc  15539  limccnpcntop  15540  limccoap  15543  dvcoapbr  15572  eflt  15640  sin0pilem2  15647  pilem3  15648  perfectlem2  15868  lgsval2lem  15883  lgsdirnn0  15920  lgsdinn0  15921  2sqlem10  15998  eupth2lem3fi  16471  subctctexmid  16774  pw1nct  16777  exmidnotnotr  16779  exmidcon  16780  exmidpeirce  16781  nnsf  16783  nninfalllem1  16786  nninfsellemeqinf  16794  isomninnlem  16814  trilpolemlt1  16825  trirec0  16828  apdiff  16832  iswomninnlem  16834  ismkvnnlem  16837  redcwlpolemeq1  16839  redc0  16842  reap0  16843  cndcap  16844  trimul0or  16845  dceqnconst  16846  dcapnconst  16847  nconstwlpolem0  16849  nconstwlpolem  16851  neap0mkv  16855  ltlenmkv  16856