Theorem rspcdva 2889

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 2880	. 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 2178   A.wral 2486

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-v 2778

This theorem is referenced by:  frirrg  4415  wetriext  4643  tfisi  4653  omsinds  4688  suppssov1  6178  caofref  6206  caofinvl  6207  caofdig  6215  oprssdmm  6280  tfrlem1  6417  tfrlem5  6423  tfr1onlemsucfn  6449  tfr1onlemsucaccv  6450  tfr1onlembxssdm  6452  tfr1onlembfn  6453  tfr1onlemaccex  6457  tfr1onlemres  6458  tfrcllemsucfn  6462  tfrcllemsucaccv  6463  tfrcllembxssdm  6465  tfrcllembfn  6466  tfrcllemaccex  6470  tfrcllemres  6471  tfrcl  6473  rdgon  6495  frecabcl  6508  pw2f1odclem  6956  undifdcss  7046  ctssdclemn0  7238  ctssdc  7241  nninfninc  7251  nnnninfeq  7256  nnnninfeq2  7257  enomnilem  7266  fodju0  7275  fodjuomnilemres  7276  ismkvnex  7283  fodjumkvlemres  7287  enmkvlem  7289  enwomnilem  7297  nninfdcinf  7299  nninfwlporlem  7301  nninfwlpoimlemdc  7305  nninfinfwlpolem  7306  exmidaclem  7351  exmidontriimlem4  7367  netap  7401  exmidapne  7407  cc2lem  7413  cc3  7415  prltlu  7635  cauappcvgprlemm  7793  caucvgprlemm  7816  caucvgprprlemml  7842  suplocexprlemmu  7866  suplocexprlemdisj  7868  suplocexprlemloc  7869  suplocexprlemub  7871  caucvgsrlemgt1  7943  caucvgsr  7950  suplocsrlemb  7954  suplocsrlempr  7955  suplocsrlem  7956  axcaucvglemcau  8046  axcaucvglemres  8047  axpre-suploclemres  8049  irrmulap  9804  suprzubdc  10416  nninfdcex  10417  zsupssdc  10418  exbtwnzlemstep  10427  apbtwnz  10454  frecuzrdgsuc  10596  frecuzrdgg  10598  frecuzrdgsuctlem  10605  uzsinds  10626  iseqovex  10640  seq3val  10642  seqvalcd  10643  seq3-1  10644  seqf  10646  seq3p1  10647  seqovcd  10649  seqp1cd  10652  seq3clss  10653  seq3fveq2  10657  seqfveq2g  10659  seqfveqg  10660  seq3fveq  10661  seq3feq  10662  seq3shft2  10663  seqshft2g  10664  monoord  10667  monoord2  10668  ser3mono  10669  seq3split  10670  seqsplitg  10671  seq3caopr3  10673  seqcaopr3g  10674  iseqf1olemkle  10679  iseqf1olemklt  10680  iseqf1olemjpcl  10690  iseqf1olemqpcl  10691  iseqf1olemfvp  10692  seq3f1olemqsumkj  10693  seq3f1olemqsum  10695  seq3f1oleml  10698  seq3f1o  10699  seqf1og  10703  seq3id3  10706  seq3id  10707  seq3id2  10708  seq3homo  10709  seq3z  10710  seqhomog  10712  seqfeq4g  10713  ser3ge0  10718  nn0ltexp2  10891  zfz1isolemiso  11021  wrdind  11213  seq3shft  11264  cvg1nlemcau  11410  cvg1nlemres  11411  recvguniq  11421  resqrexlemgt0  11446  resqrexlemoverl  11447  resqrexlemglsq  11448  climi  11713  climcn1  11734  serf0  11778  fsum3cvg  11804  summodclem2  11808  summodc  11809  fsum3  11813  isumz  11815  fsumf1o  11816  isumss  11817  fisumss  11818  isumss2  11819  fsum3cvg2  11820  fsum3cvg3  11822  fsum3ser  11823  fsumsplit  11833  fsumm1  11842  fsum1p  11844  fisumcom2  11864  fsumge1  11887  telfsumo  11892  telfsumo2  11893  fsumparts  11896  isumshft  11916  isum1p  11918  isumnn0nn  11919  isumrpcl  11920  cvgratnnlemnexp  11950  cvgratnnlemmn  11951  cvgratnnlemseq  11952  cvgratnnlemabsle  11953  cvgratnnlemfm  11955  cvgratnnlemrate  11956  cvgratnn  11957  cvgratz  11958  mertenslemi1  11961  mertenslem2  11962  mertensabs  11963  fproddccvg  11998  prodmodclem2a  12002  prodmodc  12004  zproddc  12005  fprodseq  12009  prod1dc  12012  fprodf1o  12014  prodssdc  12015  fprodssdc  12016  fprodm1  12024  fprod1p  12025  fprodcom2fi  12052  sinltxirr  12187  bezoutlemmain  12434  bezoutlemex  12437  bezoutlemzz  12438  bezoutlemmo  12442  bezoutlemle  12444  bezoutlemsup  12445  nnmindc  12470  nnminle  12471  uzwodc  12473  nninfctlemfo  12476  prmind2  12557  isprm5lem  12578  isprm5  12579  pcmpt2  12782  prmpwdvds  12793  ennnfonelemk  12886  ennnfonelemex  12900  ennnfonelemnn0  12908  ctinfomlemom  12913  ctiunctlemudc  12923  ssnnctlemct  12932  nninfdclemcl  12934  nninfdclemp1  12936  nninfdc  12939  prdsbasprj  13229  lidrideqd  13328  grpinvalem  13332  grpinva  13333  grpidd2  13488  mulgsubcl  13587  issubg4m  13644  ghmf1  13724  gsumfzmhm2  13795  lringuplu  14073  mplsubgfilemcl  14576  icnpimaex  14798  lmcvg  14804  lmff  14836  cnmpt11  14870  cnmpt21  14878  comet  15086  dedekindeulemuub  15204  dedekindeulemloc  15206  dedekindeulemlu  15208  dedekindeulemeu  15209  suplociccreex  15211  suplociccex  15212  dedekindicclemuub  15213  dedekindicclemloc  15215  dedekindicclemlu  15217  dedekindicclemeu  15218  dedekindicc  15220  ivthinclemlopn  15223  ivthinclemlr  15224  ivthinclemuopn  15225  ivthinclemur  15226  ivthinclemdisj  15227  ivthinclemloc  15228  ivthinc  15230  ivthdec  15231  ivthreinc  15232  dich0  15239  limcimolemlt  15251  limcimo  15252  cnplimclemr  15256  cnlimci  15260  cnmptlimc  15261  limccnpcntop  15262  limccoap  15265  dvcoapbr  15294  eflt  15362  sin0pilem2  15369  pilem3  15370  perfectlem2  15587  lgsval2lem  15602  lgsdirnn0  15639  lgsdinn0  15640  2sqlem10  15717  2omap  16132  subctctexmid  16139  pw1nct  16142  nnsf  16144  nninfalllem1  16147  nninfsellemeqinf  16155  isomninnlem  16171  trilpolemlt1  16182  trirec0  16185  apdiff  16189  iswomninnlem  16190  ismkvnnlem  16193  redcwlpolemeq1  16195  redc0  16198  reap0  16199  cndcap  16200  dceqnconst  16201  dcapnconst  16202  nconstwlpolem0  16204  nconstwlpolem  16206  neap0mkv  16210  ltlenmkv  16211