Theorem rspcdva 2839

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 2830	. 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 1348   e. wcel 2141   A.wral 2448

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-v 2732

This theorem is referenced by:  frirrg  4335  wetriext  4561  tfisi  4571  omsinds  4606  suppssov1  6058  caofref  6082  caofinvl  6083  oprssdmm  6150  tfrlem1  6287  tfrlem5  6293  tfr1onlemsucfn  6319  tfr1onlemsucaccv  6320  tfr1onlembxssdm  6322  tfr1onlembfn  6323  tfr1onlemaccex  6327  tfr1onlemres  6328  tfrcllemsucfn  6332  tfrcllemsucaccv  6333  tfrcllembxssdm  6335  tfrcllembfn  6336  tfrcllemaccex  6340  tfrcllemres  6341  tfrcl  6343  rdgon  6365  frecabcl  6378  undifdcss  6900  ctssdclemn0  7087  ctssdc  7090  nnnninfeq  7104  nnnninfeq2  7105  enomnilem  7114  fodju0  7123  fodjuomnilemres  7124  ismkvnex  7131  fodjumkvlemres  7135  enmkvlem  7137  enwomnilem  7145  nninfdcinf  7147  nninfwlporlem  7149  nninfwlpoimlemdc  7153  exmidaclem  7185  exmidontriimlem4  7201  cc2lem  7228  cc3  7230  prltlu  7449  cauappcvgprlemm  7607  caucvgprlemm  7630  caucvgprprlemml  7656  suplocexprlemmu  7680  suplocexprlemdisj  7682  suplocexprlemloc  7683  suplocexprlemub  7685  caucvgsrlemgt1  7757  caucvgsr  7764  suplocsrlemb  7768  suplocsrlempr  7769  suplocsrlem  7770  axcaucvglemcau  7860  axcaucvglemres  7861  axpre-suploclemres  7863  exbtwnzlemstep  10204  apbtwnz  10230  frecuzrdgsuc  10370  frecuzrdgg  10372  frecuzrdgsuctlem  10379  uzsinds  10398  iseqovex  10412  seq3val  10414  seqvalcd  10415  seq3-1  10416  seqf  10417  seq3p1  10418  seqovcd  10419  seqp1cd  10422  seq3clss  10423  seq3fveq2  10425  seq3fveq  10427  seq3feq  10428  seq3shft2  10429  monoord  10432  monoord2  10433  ser3mono  10434  seq3split  10435  seq3caopr3  10437  iseqf1olemkle  10440  iseqf1olemklt  10441  iseqf1olemjpcl  10451  iseqf1olemqpcl  10452  iseqf1olemfvp  10453  seq3f1olemqsumkj  10454  seq3f1olemqsum  10456  seq3f1oleml  10459  seq3f1o  10460  seq3id3  10463  seq3id  10464  seq3id2  10465  seq3homo  10466  seq3z  10467  ser3ge0  10473  nn0ltexp2  10644  zfz1isolemiso  10774  seq3shft  10802  cvg1nlemcau  10948  cvg1nlemres  10949  recvguniq  10959  resqrexlemgt0  10984  resqrexlemoverl  10985  resqrexlemglsq  10986  climi  11250  climcn1  11271  serf0  11315  fsum3cvg  11341  summodclem2  11345  summodc  11346  fsum3  11350  isumz  11352  fsumf1o  11353  isumss  11354  fisumss  11355  isumss2  11356  fsum3cvg2  11357  fsum3cvg3  11359  fsum3ser  11360  fsumsplit  11370  fsumm1  11379  fsum1p  11381  fisumcom2  11401  fsumge1  11424  telfsumo  11429  telfsumo2  11430  fsumparts  11433  isumshft  11453  isum1p  11455  isumnn0nn  11456  isumrpcl  11457  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  cvgratnnlemseq  11489  cvgratnnlemabsle  11490  cvgratnnlemfm  11492  cvgratnnlemrate  11493  cvgratnn  11494  cvgratz  11495  mertenslemi1  11498  mertenslem2  11499  mertensabs  11500  fproddccvg  11535  prodmodclem2a  11539  prodmodc  11541  zproddc  11542  fprodseq  11546  prod1dc  11549  fprodf1o  11551  prodssdc  11552  fprodssdc  11553  fprodm1  11561  fprod1p  11562  fprodcom2fi  11589  suprzubdc  11907  nninfdcex  11908  zsupssdc  11909  bezoutlemmain  11953  bezoutlemex  11956  bezoutlemzz  11957  bezoutlemmo  11961  bezoutlemle  11963  bezoutlemsup  11964  nnmindc  11989  nnminle  11990  uzwodc  11992  prmind2  12074  isprm5lem  12095  isprm5  12096  pcmpt2  12296  prmpwdvds  12307  ennnfonelemk  12355  ennnfonelemex  12369  ennnfonelemnn0  12377  ctinfomlemom  12382  ctiunctlemudc  12392  ssnnctlemct  12401  nninfdclemcl  12403  nninfdclemp1  12405  nninfdc  12408  lidrideqd  12635  grprinvlem  12639  grprinvd  12640  grpidd2  12744  icnpimaex  13005  lmcvg  13011  lmff  13043  cnmpt11  13077  cnmpt21  13085  comet  13293  dedekindeulemuub  13389  dedekindeulemloc  13391  dedekindeulemlu  13393  dedekindeulemeu  13394  suplociccreex  13396  suplociccex  13397  dedekindicclemuub  13398  dedekindicclemloc  13400  dedekindicclemlu  13402  dedekindicclemeu  13403  dedekindicc  13405  ivthinclemlopn  13408  ivthinclemlr  13409  ivthinclemuopn  13410  ivthinclemur  13411  ivthinclemdisj  13412  ivthinclemloc  13413  ivthinc  13415  ivthdec  13416  limcimolemlt  13427  limcimo  13428  cnplimclemr  13432  cnlimci  13436  cnmptlimc  13437  limccnpcntop  13438  limccoap  13441  dvcoapbr  13465  eflt  13490  sin0pilem2  13497  pilem3  13498  lgsval2lem  13705  lgsdirnn0  13742  lgsdinn0  13743  2sqlem10  13755  subctctexmid  14034  pw1nct  14036  nnsf  14038  nninfalllem1  14041  nninfsellemeqinf  14049  isomninnlem  14062  trilpolemlt1  14073  trirec0  14076  apdiff  14080  iswomninnlem  14081  ismkvnnlem  14084  redcwlpolemeq1  14086  redc0  14089  reap0  14090  dceqnconst  14091  dcapnconst  14092  nconstwlpolem0  14094  nconstwlpolem  14096