Theorem rspcdva 2848

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 2839	. 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 2741

This theorem is referenced by:  frirrg  4352  wetriext  4578  tfisi  4588  omsinds  4623  suppssov1  6082  caofref  6106  caofinvl  6107  oprssdmm  6174  tfrlem1  6311  tfrlem5  6317  tfr1onlemsucfn  6343  tfr1onlemsucaccv  6344  tfr1onlembxssdm  6346  tfr1onlembfn  6347  tfr1onlemaccex  6351  tfr1onlemres  6352  tfrcllemsucfn  6356  tfrcllemsucaccv  6357  tfrcllembxssdm  6359  tfrcllembfn  6360  tfrcllemaccex  6364  tfrcllemres  6365  tfrcl  6367  rdgon  6389  frecabcl  6402  undifdcss  6924  ctssdclemn0  7111  ctssdc  7114  nnnninfeq  7128  nnnninfeq2  7129  enomnilem  7138  fodju0  7147  fodjuomnilemres  7148  ismkvnex  7155  fodjumkvlemres  7159  enmkvlem  7161  enwomnilem  7169  nninfdcinf  7171  nninfwlporlem  7173  nninfwlpoimlemdc  7177  exmidaclem  7209  exmidontriimlem4  7225  netap  7255  exmidapne  7261  cc2lem  7267  cc3  7269  prltlu  7488  cauappcvgprlemm  7646  caucvgprlemm  7669  caucvgprprlemml  7695  suplocexprlemmu  7719  suplocexprlemdisj  7721  suplocexprlemloc  7722  suplocexprlemub  7724  caucvgsrlemgt1  7796  caucvgsr  7803  suplocsrlemb  7807  suplocsrlempr  7808  suplocsrlem  7809  axcaucvglemcau  7899  axcaucvglemres  7900  axpre-suploclemres  7902  exbtwnzlemstep  10250  apbtwnz  10276  frecuzrdgsuc  10416  frecuzrdgg  10418  frecuzrdgsuctlem  10425  uzsinds  10444  iseqovex  10458  seq3val  10460  seqvalcd  10461  seq3-1  10462  seqf  10463  seq3p1  10464  seqovcd  10465  seqp1cd  10468  seq3clss  10469  seq3fveq2  10471  seq3fveq  10473  seq3feq  10474  seq3shft2  10475  monoord  10478  monoord2  10479  ser3mono  10480  seq3split  10481  seq3caopr3  10483  iseqf1olemkle  10486  iseqf1olemklt  10487  iseqf1olemjpcl  10497  iseqf1olemqpcl  10498  iseqf1olemfvp  10499  seq3f1olemqsumkj  10500  seq3f1olemqsum  10502  seq3f1oleml  10505  seq3f1o  10506  seq3id3  10509  seq3id  10510  seq3id2  10511  seq3homo  10512  seq3z  10513  ser3ge0  10519  nn0ltexp2  10691  zfz1isolemiso  10821  seq3shft  10849  cvg1nlemcau  10995  cvg1nlemres  10996  recvguniq  11006  resqrexlemgt0  11031  resqrexlemoverl  11032  resqrexlemglsq  11033  climi  11297  climcn1  11318  serf0  11362  fsum3cvg  11388  summodclem2  11392  summodc  11393  fsum3  11397  isumz  11399  fsumf1o  11400  isumss  11401  fisumss  11402  isumss2  11403  fsum3cvg2  11404  fsum3cvg3  11406  fsum3ser  11407  fsumsplit  11417  fsumm1  11426  fsum1p  11428  fisumcom2  11448  fsumge1  11471  telfsumo  11476  telfsumo2  11477  fsumparts  11480  isumshft  11500  isum1p  11502  isumnn0nn  11503  isumrpcl  11504  cvgratnnlemnexp  11534  cvgratnnlemmn  11535  cvgratnnlemseq  11536  cvgratnnlemabsle  11537  cvgratnnlemfm  11539  cvgratnnlemrate  11540  cvgratnn  11541  cvgratz  11542  mertenslemi1  11545  mertenslem2  11546  mertensabs  11547  fproddccvg  11582  prodmodclem2a  11586  prodmodc  11588  zproddc  11589  fprodseq  11593  prod1dc  11596  fprodf1o  11598  prodssdc  11599  fprodssdc  11600  fprodm1  11608  fprod1p  11609  fprodcom2fi  11636  suprzubdc  11955  nninfdcex  11956  zsupssdc  11957  bezoutlemmain  12001  bezoutlemex  12004  bezoutlemzz  12005  bezoutlemmo  12009  bezoutlemle  12011  bezoutlemsup  12012  nnmindc  12037  nnminle  12038  uzwodc  12040  prmind2  12122  isprm5lem  12143  isprm5  12144  pcmpt2  12344  prmpwdvds  12355  ennnfonelemk  12403  ennnfonelemex  12417  ennnfonelemnn0  12425  ctinfomlemom  12430  ctiunctlemudc  12440  ssnnctlemct  12449  nninfdclemcl  12451  nninfdclemp1  12453  nninfdc  12456  lidrideqd  12805  grprinvlem  12809  grprinvd  12810  grpidd2  12919  mulgsubcl  13002  issubg4m  13058  lringuplu  13342  icnpimaex  13750  lmcvg  13756  lmff  13788  cnmpt11  13822  cnmpt21  13830  comet  14038  dedekindeulemuub  14134  dedekindeulemloc  14136  dedekindeulemlu  14138  dedekindeulemeu  14139  suplociccreex  14141  suplociccex  14142  dedekindicclemuub  14143  dedekindicclemloc  14145  dedekindicclemlu  14147  dedekindicclemeu  14148  dedekindicc  14150  ivthinclemlopn  14153  ivthinclemlr  14154  ivthinclemuopn  14155  ivthinclemur  14156  ivthinclemdisj  14157  ivthinclemloc  14158  ivthinc  14160  ivthdec  14161  limcimolemlt  14172  limcimo  14173  cnplimclemr  14177  cnlimci  14181  cnmptlimc  14182  limccnpcntop  14183  limccoap  14186  dvcoapbr  14210  eflt  14235  sin0pilem2  14242  pilem3  14243  lgsval2lem  14450  lgsdirnn0  14487  lgsdinn0  14488  2sqlem10  14511  subctctexmid  14789  pw1nct  14791  nnsf  14793  nninfalllem1  14796  nninfsellemeqinf  14804  isomninnlem  14817  trilpolemlt1  14828  trirec0  14831  apdiff  14835  iswomninnlem  14836  ismkvnnlem  14839  redcwlpolemeq1  14841  redc0  14844  reap0  14845  cndcap  14846  dceqnconst  14847  dcapnconst  14848  nconstwlpolem0  14850  nconstwlpolem  14852  neap0mkv  14856  ltlenmkv  14857