Theorem rspcdva 2846

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 2837	. 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 1353   e. wcel 2148   A.wral 2455

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-v 2739

This theorem is referenced by:  frirrg  4348  wetriext  4574  tfisi  4584  omsinds  4619  suppssov1  6075  caofref  6099  caofinvl  6100  oprssdmm  6167  tfrlem1  6304  tfrlem5  6310  tfr1onlemsucfn  6336  tfr1onlemsucaccv  6337  tfr1onlembxssdm  6339  tfr1onlembfn  6340  tfr1onlemaccex  6344  tfr1onlemres  6345  tfrcllemsucfn  6349  tfrcllemsucaccv  6350  tfrcllembxssdm  6352  tfrcllembfn  6353  tfrcllemaccex  6357  tfrcllemres  6358  tfrcl  6360  rdgon  6382  frecabcl  6395  undifdcss  6917  ctssdclemn0  7104  ctssdc  7107  nnnninfeq  7121  nnnninfeq2  7122  enomnilem  7131  fodju0  7140  fodjuomnilemres  7141  ismkvnex  7148  fodjumkvlemres  7152  enmkvlem  7154  enwomnilem  7162  nninfdcinf  7164  nninfwlporlem  7166  nninfwlpoimlemdc  7170  exmidaclem  7202  exmidontriimlem4  7218  netap  7248  exmidapne  7254  cc2lem  7260  cc3  7262  prltlu  7481  cauappcvgprlemm  7639  caucvgprlemm  7662  caucvgprprlemml  7688  suplocexprlemmu  7712  suplocexprlemdisj  7714  suplocexprlemloc  7715  suplocexprlemub  7717  caucvgsrlemgt1  7789  caucvgsr  7796  suplocsrlemb  7800  suplocsrlempr  7801  suplocsrlem  7802  axcaucvglemcau  7892  axcaucvglemres  7893  axpre-suploclemres  7895  exbtwnzlemstep  10241  apbtwnz  10267  frecuzrdgsuc  10407  frecuzrdgg  10409  frecuzrdgsuctlem  10416  uzsinds  10435  iseqovex  10449  seq3val  10451  seqvalcd  10452  seq3-1  10453  seqf  10454  seq3p1  10455  seqovcd  10456  seqp1cd  10459  seq3clss  10460  seq3fveq2  10462  seq3fveq  10464  seq3feq  10465  seq3shft2  10466  monoord  10469  monoord2  10470  ser3mono  10471  seq3split  10472  seq3caopr3  10474  iseqf1olemkle  10477  iseqf1olemklt  10478  iseqf1olemjpcl  10488  iseqf1olemqpcl  10489  iseqf1olemfvp  10490  seq3f1olemqsumkj  10491  seq3f1olemqsum  10493  seq3f1oleml  10496  seq3f1o  10497  seq3id3  10500  seq3id  10501  seq3id2  10502  seq3homo  10503  seq3z  10504  ser3ge0  10510  nn0ltexp2  10681  zfz1isolemiso  10810  seq3shft  10838  cvg1nlemcau  10984  cvg1nlemres  10985  recvguniq  10995  resqrexlemgt0  11020  resqrexlemoverl  11021  resqrexlemglsq  11022  climi  11286  climcn1  11307  serf0  11351  fsum3cvg  11377  summodclem2  11381  summodc  11382  fsum3  11386  isumz  11388  fsumf1o  11389  isumss  11390  fisumss  11391  isumss2  11392  fsum3cvg2  11393  fsum3cvg3  11395  fsum3ser  11396  fsumsplit  11406  fsumm1  11415  fsum1p  11417  fisumcom2  11437  fsumge1  11460  telfsumo  11465  telfsumo2  11466  fsumparts  11469  isumshft  11489  isum1p  11491  isumnn0nn  11492  isumrpcl  11493  cvgratnnlemnexp  11523  cvgratnnlemmn  11524  cvgratnnlemseq  11525  cvgratnnlemabsle  11526  cvgratnnlemfm  11528  cvgratnnlemrate  11529  cvgratnn  11530  cvgratz  11531  mertenslemi1  11534  mertenslem2  11535  mertensabs  11536  fproddccvg  11571  prodmodclem2a  11575  prodmodc  11577  zproddc  11578  fprodseq  11582  prod1dc  11585  fprodf1o  11587  prodssdc  11588  fprodssdc  11589  fprodm1  11597  fprod1p  11598  fprodcom2fi  11625  suprzubdc  11943  nninfdcex  11944  zsupssdc  11945  bezoutlemmain  11989  bezoutlemex  11992  bezoutlemzz  11993  bezoutlemmo  11997  bezoutlemle  11999  bezoutlemsup  12000  nnmindc  12025  nnminle  12026  uzwodc  12028  prmind2  12110  isprm5lem  12131  isprm5  12132  pcmpt2  12332  prmpwdvds  12343  ennnfonelemk  12391  ennnfonelemex  12405  ennnfonelemnn0  12413  ctinfomlemom  12418  ctiunctlemudc  12428  ssnnctlemct  12437  nninfdclemcl  12439  nninfdclemp1  12441  nninfdc  12444  lidrideqd  12730  grprinvlem  12734  grprinvd  12735  grpidd2  12842  mulgsubcl  12925  issubg4m  12979  lringuplu  13236  icnpimaex  13493  lmcvg  13499  lmff  13531  cnmpt11  13565  cnmpt21  13573  comet  13781  dedekindeulemuub  13877  dedekindeulemloc  13879  dedekindeulemlu  13881  dedekindeulemeu  13882  suplociccreex  13884  suplociccex  13885  dedekindicclemuub  13886  dedekindicclemloc  13888  dedekindicclemlu  13890  dedekindicclemeu  13891  dedekindicc  13893  ivthinclemlopn  13896  ivthinclemlr  13897  ivthinclemuopn  13898  ivthinclemur  13899  ivthinclemdisj  13900  ivthinclemloc  13901  ivthinc  13903  ivthdec  13904  limcimolemlt  13915  limcimo  13916  cnplimclemr  13920  cnlimci  13924  cnmptlimc  13925  limccnpcntop  13926  limccoap  13929  dvcoapbr  13953  eflt  13978  sin0pilem2  13985  pilem3  13986  lgsval2lem  14193  lgsdirnn0  14230  lgsdinn0  14231  2sqlem10  14243  subctctexmid  14521  pw1nct  14523  nnsf  14525  nninfalllem1  14528  nninfsellemeqinf  14536  isomninnlem  14549  trilpolemlt1  14560  trirec0  14563  apdiff  14567  iswomninnlem  14568  ismkvnnlem  14571  redcwlpolemeq1  14573  redc0  14576  reap0  14577  dceqnconst  14578  dcapnconst  14579  nconstwlpolem0  14581  nconstwlpolem  14583  neap0mkv  14587  ltlenmkv  14588