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  4397  wetriext  4625  tfisi  4635  omsinds  4670  suppssov1  6155  caofref  6183  caofinvl  6184  caofdig  6192  oprssdmm  6257  tfrlem1  6394  tfrlem5  6400  tfr1onlemsucfn  6426  tfr1onlemsucaccv  6427  tfr1onlembxssdm  6429  tfr1onlembfn  6430  tfr1onlemaccex  6434  tfr1onlemres  6435  tfrcllemsucfn  6439  tfrcllemsucaccv  6440  tfrcllembxssdm  6442  tfrcllembfn  6443  tfrcllemaccex  6447  tfrcllemres  6448  tfrcl  6450  rdgon  6472  frecabcl  6485  pw2f1odclem  6931  undifdcss  7020  ctssdclemn0  7212  ctssdc  7215  nninfninc  7225  nnnninfeq  7230  nnnninfeq2  7231  enomnilem  7240  fodju0  7249  fodjuomnilemres  7250  ismkvnex  7257  fodjumkvlemres  7261  enmkvlem  7263  enwomnilem  7271  nninfdcinf  7273  nninfwlporlem  7275  nninfwlpoimlemdc  7279  nninfinfwlpolem  7280  exmidaclem  7320  exmidontriimlem4  7336  netap  7366  exmidapne  7372  cc2lem  7378  cc3  7380  prltlu  7600  cauappcvgprlemm  7758  caucvgprlemm  7781  caucvgprprlemml  7807  suplocexprlemmu  7831  suplocexprlemdisj  7833  suplocexprlemloc  7834  suplocexprlemub  7836  caucvgsrlemgt1  7908  caucvgsr  7915  suplocsrlemb  7919  suplocsrlempr  7920  suplocsrlem  7921  axcaucvglemcau  8011  axcaucvglemres  8012  axpre-suploclemres  8014  irrmulap  9769  suprzubdc  10379  nninfdcex  10380  zsupssdc  10381  exbtwnzlemstep  10390  apbtwnz  10417  frecuzrdgsuc  10559  frecuzrdgg  10561  frecuzrdgsuctlem  10568  uzsinds  10589  iseqovex  10603  seq3val  10605  seqvalcd  10606  seq3-1  10607  seqf  10609  seq3p1  10610  seqovcd  10612  seqp1cd  10615  seq3clss  10616  seq3fveq2  10620  seqfveq2g  10622  seqfveqg  10623  seq3fveq  10624  seq3feq  10625  seq3shft2  10626  seqshft2g  10627  monoord  10630  monoord2  10631  ser3mono  10632  seq3split  10633  seqsplitg  10634  seq3caopr3  10636  seqcaopr3g  10637  iseqf1olemkle  10642  iseqf1olemklt  10643  iseqf1olemjpcl  10653  iseqf1olemqpcl  10654  iseqf1olemfvp  10655  seq3f1olemqsumkj  10656  seq3f1olemqsum  10658  seq3f1oleml  10661  seq3f1o  10662  seqf1og  10666  seq3id3  10669  seq3id  10670  seq3id2  10671  seq3homo  10672  seq3z  10673  seqhomog  10675  seqfeq4g  10676  ser3ge0  10681  nn0ltexp2  10854  zfz1isolemiso  10984  seq3shft  11149  cvg1nlemcau  11295  cvg1nlemres  11296  recvguniq  11306  resqrexlemgt0  11331  resqrexlemoverl  11332  resqrexlemglsq  11333  climi  11598  climcn1  11619  serf0  11663  fsum3cvg  11689  summodclem2  11693  summodc  11694  fsum3  11698  isumz  11700  fsumf1o  11701  isumss  11702  fisumss  11703  isumss2  11704  fsum3cvg2  11705  fsum3cvg3  11707  fsum3ser  11708  fsumsplit  11718  fsumm1  11727  fsum1p  11729  fisumcom2  11749  fsumge1  11772  telfsumo  11777  telfsumo2  11778  fsumparts  11781  isumshft  11801  isum1p  11803  isumnn0nn  11804  isumrpcl  11805  cvgratnnlemnexp  11835  cvgratnnlemmn  11836  cvgratnnlemseq  11837  cvgratnnlemabsle  11838  cvgratnnlemfm  11840  cvgratnnlemrate  11841  cvgratnn  11842  cvgratz  11843  mertenslemi1  11846  mertenslem2  11847  mertensabs  11848  fproddccvg  11883  prodmodclem2a  11887  prodmodc  11889  zproddc  11890  fprodseq  11894  prod1dc  11897  fprodf1o  11899  prodssdc  11900  fprodssdc  11901  fprodm1  11909  fprod1p  11910  fprodcom2fi  11937  sinltxirr  12072  bezoutlemmain  12319  bezoutlemex  12322  bezoutlemzz  12323  bezoutlemmo  12327  bezoutlemle  12329  bezoutlemsup  12330  nnmindc  12355  nnminle  12356  uzwodc  12358  nninfctlemfo  12361  prmind2  12442  isprm5lem  12463  isprm5  12464  pcmpt2  12667  prmpwdvds  12678  ennnfonelemk  12771  ennnfonelemex  12785  ennnfonelemnn0  12793  ctinfomlemom  12798  ctiunctlemudc  12808  ssnnctlemct  12817  nninfdclemcl  12819  nninfdclemp1  12821  nninfdc  12824  prdsbasprj  13114  lidrideqd  13213  grpinvalem  13217  grpinva  13218  grpidd2  13373  mulgsubcl  13472  issubg4m  13529  ghmf1  13609  gsumfzmhm2  13680  lringuplu  13958  mplsubgfilemcl  14461  icnpimaex  14683  lmcvg  14689  lmff  14721  cnmpt11  14755  cnmpt21  14763  comet  14971  dedekindeulemuub  15089  dedekindeulemloc  15091  dedekindeulemlu  15093  dedekindeulemeu  15094  suplociccreex  15096  suplociccex  15097  dedekindicclemuub  15098  dedekindicclemloc  15100  dedekindicclemlu  15102  dedekindicclemeu  15103  dedekindicc  15105  ivthinclemlopn  15108  ivthinclemlr  15109  ivthinclemuopn  15110  ivthinclemur  15111  ivthinclemdisj  15112  ivthinclemloc  15113  ivthinc  15115  ivthdec  15116  ivthreinc  15117  dich0  15124  limcimolemlt  15136  limcimo  15137  cnplimclemr  15141  cnlimci  15145  cnmptlimc  15146  limccnpcntop  15147  limccoap  15150  dvcoapbr  15179  eflt  15247  sin0pilem2  15254  pilem3  15255  perfectlem2  15472  lgsval2lem  15487  lgsdirnn0  15524  lgsdinn0  15525  2sqlem10  15602  2omap  15932  subctctexmid  15937  pw1nct  15940  nnsf  15942  nninfalllem1  15945  nninfsellemeqinf  15953  isomninnlem  15969  trilpolemlt1  15980  trirec0  15983  apdiff  15987  iswomninnlem  15988  ismkvnnlem  15991  redcwlpolemeq1  15993  redc0  15996  reap0  15997  cndcap  15998  dceqnconst  15999  dcapnconst  16000  nconstwlpolem0  16002  nconstwlpolem  16004  neap0mkv  16008  ltlenmkv  16009