Theorem rspcdva 2798

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 2789	. 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 1332   e. wcel 1481   A.wral 2417

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-v 2691

This theorem is referenced by:  frirrg  4280  wetriext  4499  tfisi  4509  omsinds  4543  grprinvlem  5973  grprinvd  5974  suppssov1  5987  caofref  6011  caofinvl  6012  oprssdmm  6077  tfrlem1  6213  tfrlem5  6219  tfr1onlemsucfn  6245  tfr1onlemsucaccv  6246  tfr1onlembxssdm  6248  tfr1onlembfn  6249  tfr1onlemaccex  6253  tfr1onlemres  6254  tfrcllemsucfn  6258  tfrcllemsucaccv  6259  tfrcllembxssdm  6261  tfrcllembfn  6262  tfrcllemaccex  6266  tfrcllemres  6267  tfrcl  6269  rdgon  6291  frecabcl  6304  undifdcss  6819  ctssdclemn0  7003  ctssdc  7006  enomnilem  7018  fodju0  7027  fodjuomnilemres  7028  ismkvnex  7037  fodjumkvlemres  7041  enmkvlem  7043  enwomnilem  7050  exmidaclem  7081  cc2lem  7098  cc3  7100  prltlu  7319  cauappcvgprlemm  7477  caucvgprlemm  7500  caucvgprprlemml  7526  suplocexprlemmu  7550  suplocexprlemdisj  7552  suplocexprlemloc  7553  suplocexprlemub  7555  caucvgsrlemgt1  7627  caucvgsr  7634  suplocsrlemb  7638  suplocsrlempr  7639  suplocsrlem  7640  axcaucvglemcau  7730  axcaucvglemres  7731  axpre-suploclemres  7733  exbtwnzlemstep  10056  apbtwnz  10078  frecuzrdgsuc  10218  frecuzrdgg  10220  frecuzrdgsuctlem  10227  uzsinds  10246  iseqovex  10260  seq3val  10262  seqvalcd  10263  seq3-1  10264  seqf  10265  seq3p1  10266  seqovcd  10267  seqp1cd  10270  seq3clss  10271  seq3fveq2  10273  seq3fveq  10275  seq3feq  10276  seq3shft2  10277  monoord  10280  monoord2  10281  ser3mono  10282  seq3split  10283  seq3caopr3  10285  iseqf1olemkle  10288  iseqf1olemklt  10289  iseqf1olemjpcl  10299  iseqf1olemqpcl  10300  iseqf1olemfvp  10301  seq3f1olemqsumkj  10302  seq3f1olemqsum  10304  seq3f1oleml  10307  seq3f1o  10308  seq3id3  10311  seq3id  10312  seq3id2  10313  seq3homo  10314  seq3z  10315  ser3ge0  10321  zfz1isolemiso  10614  seq3shft  10642  cvg1nlemcau  10788  cvg1nlemres  10789  recvguniq  10799  resqrexlemgt0  10824  resqrexlemoverl  10825  resqrexlemglsq  10826  climi  11088  climcn1  11109  serf0  11153  fsum3cvg  11179  summodclem2  11183  summodc  11184  fsum3  11188  isumz  11190  fsumf1o  11191  isumss  11192  fisumss  11193  isumss2  11194  fsum3cvg2  11195  fsum3cvg3  11197  fsum3ser  11198  fsumsplit  11208  fsumm1  11217  fsum1p  11219  fisumcom2  11239  fsumge1  11262  telfsumo  11267  telfsumo2  11268  fsumparts  11271  isumshft  11291  isum1p  11293  isumnn0nn  11294  isumrpcl  11295  cvgratnnlemnexp  11325  cvgratnnlemmn  11326  cvgratnnlemseq  11327  cvgratnnlemabsle  11328  cvgratnnlemfm  11330  cvgratnnlemrate  11331  cvgratnn  11332  cvgratz  11333  mertenslemi1  11336  mertenslem2  11337  mertensabs  11338  fproddccvg  11373  prodmodclem2a  11377  prodmodc  11379  zproddc  11380  fprodseq  11384  bezoutlemmain  11722  bezoutlemex  11725  bezoutlemzz  11726  bezoutlemmo  11730  bezoutlemle  11732  bezoutlemsup  11733  prmind2  11837  ennnfonelemk  11949  ennnfonelemex  11963  ennnfonelemnn0  11971  ctinfomlemom  11976  ctiunctlemudc  11986  icnpimaex  12419  lmcvg  12425  lmff  12457  cnmpt11  12491  cnmpt21  12499  comet  12707  dedekindeulemuub  12803  dedekindeulemloc  12805  dedekindeulemlu  12807  dedekindeulemeu  12808  suplociccreex  12810  suplociccex  12811  dedekindicclemuub  12812  dedekindicclemloc  12814  dedekindicclemlu  12816  dedekindicclemeu  12817  dedekindicc  12819  ivthinclemlopn  12822  ivthinclemlr  12823  ivthinclemuopn  12824  ivthinclemur  12825  ivthinclemdisj  12826  ivthinclemloc  12827  ivthinc  12829  ivthdec  12830  limcimolemlt  12841  limcimo  12842  cnplimclemr  12846  cnlimci  12850  cnmptlimc  12851  limccnpcntop  12852  limccoap  12855  dvcoapbr  12879  eflt  12904  sin0pilem2  12911  pilem3  12912  subctctexmid  13369  pw1nct  13371  nnsf  13374  nninfalllemn  13377  nninfalllem1  13378  nninfsellemeqinf  13387  isomninnlem  13400  trilpolemlt1  13409  trirec0  13412  apdiff  13416  iswomninnlem  13417  ismkvnnlem  13419  redcwlpolemeq1  13421  dceqnconst  13423