Theorem rspcdva 2821

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 2812	. 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 1335   e. wcel 2128   A.wral 2435

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 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-v 2714

This theorem is referenced by:  frirrg  4313  wetriext  4539  tfisi  4549  omsinds  4584  grprinvlem  6018  grprinvd  6019  suppssov1  6032  caofref  6056  caofinvl  6057  oprssdmm  6122  tfrlem1  6258  tfrlem5  6264  tfr1onlemsucfn  6290  tfr1onlemsucaccv  6291  tfr1onlembxssdm  6293  tfr1onlembfn  6294  tfr1onlemaccex  6298  tfr1onlemres  6299  tfrcllemsucfn  6303  tfrcllemsucaccv  6304  tfrcllembxssdm  6306  tfrcllembfn  6307  tfrcllemaccex  6311  tfrcllemres  6312  tfrcl  6314  rdgon  6336  frecabcl  6349  undifdcss  6870  ctssdclemn0  7057  ctssdc  7060  nnnninfeq  7074  nnnninfeq2  7075  enomnilem  7084  fodju0  7093  fodjuomnilemres  7094  ismkvnex  7101  fodjumkvlemres  7105  enmkvlem  7107  enwomnilem  7115  exmidaclem  7146  exmidontriimlem4  7162  cc2lem  7189  cc3  7191  prltlu  7410  cauappcvgprlemm  7568  caucvgprlemm  7591  caucvgprprlemml  7617  suplocexprlemmu  7641  suplocexprlemdisj  7643  suplocexprlemloc  7644  suplocexprlemub  7646  caucvgsrlemgt1  7718  caucvgsr  7725  suplocsrlemb  7729  suplocsrlempr  7730  suplocsrlem  7731  axcaucvglemcau  7821  axcaucvglemres  7822  axpre-suploclemres  7824  exbtwnzlemstep  10157  apbtwnz  10183  frecuzrdgsuc  10323  frecuzrdgg  10325  frecuzrdgsuctlem  10332  uzsinds  10351  iseqovex  10365  seq3val  10367  seqvalcd  10368  seq3-1  10369  seqf  10370  seq3p1  10371  seqovcd  10372  seqp1cd  10375  seq3clss  10376  seq3fveq2  10378  seq3fveq  10380  seq3feq  10381  seq3shft2  10382  monoord  10385  monoord2  10386  ser3mono  10387  seq3split  10388  seq3caopr3  10390  iseqf1olemkle  10393  iseqf1olemklt  10394  iseqf1olemjpcl  10404  iseqf1olemqpcl  10405  iseqf1olemfvp  10406  seq3f1olemqsumkj  10407  seq3f1olemqsum  10409  seq3f1oleml  10412  seq3f1o  10413  seq3id3  10416  seq3id  10417  seq3id2  10418  seq3homo  10419  seq3z  10420  ser3ge0  10426  nn0ltexp2  10596  zfz1isolemiso  10722  seq3shft  10750  cvg1nlemcau  10896  cvg1nlemres  10897  recvguniq  10907  resqrexlemgt0  10932  resqrexlemoverl  10933  resqrexlemglsq  10934  climi  11196  climcn1  11217  serf0  11261  fsum3cvg  11287  summodclem2  11291  summodc  11292  fsum3  11296  isumz  11298  fsumf1o  11299  isumss  11300  fisumss  11301  isumss2  11302  fsum3cvg2  11303  fsum3cvg3  11305  fsum3ser  11306  fsumsplit  11316  fsumm1  11325  fsum1p  11327  fisumcom2  11347  fsumge1  11370  telfsumo  11375  telfsumo2  11376  fsumparts  11379  isumshft  11399  isum1p  11401  isumnn0nn  11402  isumrpcl  11403  cvgratnnlemnexp  11433  cvgratnnlemmn  11434  cvgratnnlemseq  11435  cvgratnnlemabsle  11436  cvgratnnlemfm  11438  cvgratnnlemrate  11439  cvgratnn  11440  cvgratz  11441  mertenslemi1  11444  mertenslem2  11445  mertensabs  11446  fproddccvg  11481  prodmodclem2a  11485  prodmodc  11487  zproddc  11488  fprodseq  11492  prod1dc  11495  fprodf1o  11497  prodssdc  11498  fprodssdc  11499  fprodm1  11507  fprod1p  11508  fprodcom2fi  11535  suprzubdc  11852  nninfdcex  11853  zsupssdc  11854  bezoutlemmain  11898  bezoutlemex  11901  bezoutlemzz  11902  bezoutlemmo  11906  bezoutlemle  11908  bezoutlemsup  11909  prmind2  12013  ennnfonelemk  12225  ennnfonelemex  12239  ennnfonelemnn0  12247  ctinfomlemom  12252  ctiunctlemudc  12262  ssnnctlemct  12271  nnmindc  12273  nnminle  12274  nninfdclemcl  12275  nninfdclemp1  12277  nninfdc  12280  icnpimaex  12707  lmcvg  12713  lmff  12745  cnmpt11  12779  cnmpt21  12787  comet  12995  dedekindeulemuub  13091  dedekindeulemloc  13093  dedekindeulemlu  13095  dedekindeulemeu  13096  suplociccreex  13098  suplociccex  13099  dedekindicclemuub  13100  dedekindicclemloc  13102  dedekindicclemlu  13104  dedekindicclemeu  13105  dedekindicc  13107  ivthinclemlopn  13110  ivthinclemlr  13111  ivthinclemuopn  13112  ivthinclemur  13113  ivthinclemdisj  13114  ivthinclemloc  13115  ivthinc  13117  ivthdec  13118  limcimolemlt  13129  limcimo  13130  cnplimclemr  13134  cnlimci  13138  cnmptlimc  13139  limccnpcntop  13140  limccoap  13143  dvcoapbr  13167  eflt  13192  sin0pilem2  13199  pilem3  13200  subctctexmid  13670  pw1nct  13672  nnsf  13674  nninfalllem1  13677  nninfsellemeqinf  13685  isomninnlem  13698  trilpolemlt1  13709  trirec0  13712  apdiff  13716  iswomninnlem  13717  ismkvnnlem  13720  redcwlpolemeq1  13722  redc0  13725  reap0  13726  dceqnconst  13727  dcapnconst  13728  nconstwlpolem0  13730  nconstwlpolem  13732