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  6083  caofref  6107  caofinvl  6108  oprssdmm  6175  tfrlem1  6312  tfrlem5  6318  tfr1onlemsucfn  6344  tfr1onlemsucaccv  6345  tfr1onlembxssdm  6347  tfr1onlembfn  6348  tfr1onlemaccex  6352  tfr1onlemres  6353  tfrcllemsucfn  6357  tfrcllemsucaccv  6358  tfrcllembxssdm  6360  tfrcllembfn  6361  tfrcllemaccex  6365  tfrcllemres  6366  tfrcl  6368  rdgon  6390  frecabcl  6403  undifdcss  6925  ctssdclemn0  7112  ctssdc  7115  nnnninfeq  7129  nnnninfeq2  7130  enomnilem  7139  fodju0  7148  fodjuomnilemres  7149  ismkvnex  7156  fodjumkvlemres  7160  enmkvlem  7162  enwomnilem  7170  nninfdcinf  7172  nninfwlporlem  7174  nninfwlpoimlemdc  7178  exmidaclem  7210  exmidontriimlem4  7226  netap  7256  exmidapne  7262  cc2lem  7268  cc3  7270  prltlu  7489  cauappcvgprlemm  7647  caucvgprlemm  7670  caucvgprprlemml  7696  suplocexprlemmu  7720  suplocexprlemdisj  7722  suplocexprlemloc  7723  suplocexprlemub  7725  caucvgsrlemgt1  7797  caucvgsr  7804  suplocsrlemb  7808  suplocsrlempr  7809  suplocsrlem  7810  axcaucvglemcau  7900  axcaucvglemres  7901  axpre-suploclemres  7903  exbtwnzlemstep  10251  apbtwnz  10277  frecuzrdgsuc  10417  frecuzrdgg  10419  frecuzrdgsuctlem  10426  uzsinds  10445  iseqovex  10459  seq3val  10461  seqvalcd  10462  seq3-1  10463  seqf  10464  seq3p1  10465  seqovcd  10466  seqp1cd  10469  seq3clss  10470  seq3fveq2  10472  seq3fveq  10474  seq3feq  10475  seq3shft2  10476  monoord  10479  monoord2  10480  ser3mono  10481  seq3split  10482  seq3caopr3  10484  iseqf1olemkle  10487  iseqf1olemklt  10488  iseqf1olemjpcl  10498  iseqf1olemqpcl  10499  iseqf1olemfvp  10500  seq3f1olemqsumkj  10501  seq3f1olemqsum  10503  seq3f1oleml  10506  seq3f1o  10507  seq3id3  10510  seq3id  10511  seq3id2  10512  seq3homo  10513  seq3z  10514  ser3ge0  10520  nn0ltexp2  10692  zfz1isolemiso  10822  seq3shft  10850  cvg1nlemcau  10996  cvg1nlemres  10997  recvguniq  11007  resqrexlemgt0  11032  resqrexlemoverl  11033  resqrexlemglsq  11034  climi  11298  climcn1  11319  serf0  11363  fsum3cvg  11389  summodclem2  11393  summodc  11394  fsum3  11398  isumz  11400  fsumf1o  11401  isumss  11402  fisumss  11403  isumss2  11404  fsum3cvg2  11405  fsum3cvg3  11407  fsum3ser  11408  fsumsplit  11418  fsumm1  11427  fsum1p  11429  fisumcom2  11449  fsumge1  11472  telfsumo  11477  telfsumo2  11478  fsumparts  11481  isumshft  11501  isum1p  11503  isumnn0nn  11504  isumrpcl  11505  cvgratnnlemnexp  11535  cvgratnnlemmn  11536  cvgratnnlemseq  11537  cvgratnnlemabsle  11538  cvgratnnlemfm  11540  cvgratnnlemrate  11541  cvgratnn  11542  cvgratz  11543  mertenslemi1  11546  mertenslem2  11547  mertensabs  11548  fproddccvg  11583  prodmodclem2a  11587  prodmodc  11589  zproddc  11590  fprodseq  11594  prod1dc  11597  fprodf1o  11599  prodssdc  11600  fprodssdc  11601  fprodm1  11609  fprod1p  11610  fprodcom2fi  11637  suprzubdc  11956  nninfdcex  11957  zsupssdc  11958  bezoutlemmain  12002  bezoutlemex  12005  bezoutlemzz  12006  bezoutlemmo  12010  bezoutlemle  12012  bezoutlemsup  12013  nnmindc  12038  nnminle  12039  uzwodc  12041  prmind2  12123  isprm5lem  12144  isprm5  12145  pcmpt2  12345  prmpwdvds  12356  ennnfonelemk  12404  ennnfonelemex  12418  ennnfonelemnn0  12426  ctinfomlemom  12431  ctiunctlemudc  12441  ssnnctlemct  12450  nninfdclemcl  12452  nninfdclemp1  12454  nninfdc  12457  lidrideqd  12807  grprinvlem  12811  grprinvd  12812  grpidd2  12921  mulgsubcl  13007  issubg4m  13063  lringuplu  13348  icnpimaex  13872  lmcvg  13878  lmff  13910  cnmpt11  13944  cnmpt21  13952  comet  14160  dedekindeulemuub  14256  dedekindeulemloc  14258  dedekindeulemlu  14260  dedekindeulemeu  14261  suplociccreex  14263  suplociccex  14264  dedekindicclemuub  14265  dedekindicclemloc  14267  dedekindicclemlu  14269  dedekindicclemeu  14270  dedekindicc  14272  ivthinclemlopn  14275  ivthinclemlr  14276  ivthinclemuopn  14277  ivthinclemur  14278  ivthinclemdisj  14279  ivthinclemloc  14280  ivthinc  14282  ivthdec  14283  limcimolemlt  14294  limcimo  14295  cnplimclemr  14299  cnlimci  14303  cnmptlimc  14304  limccnpcntop  14305  limccoap  14308  dvcoapbr  14332  eflt  14357  sin0pilem2  14364  pilem3  14365  lgsval2lem  14572  lgsdirnn0  14609  lgsdinn0  14610  2sqlem10  14633  subctctexmid  14912  pw1nct  14914  nnsf  14916  nninfalllem1  14919  nninfsellemeqinf  14927  isomninnlem  14940  trilpolemlt1  14951  trirec0  14954  apdiff  14958  iswomninnlem  14959  ismkvnnlem  14962  redcwlpolemeq1  14964  redc0  14967  reap0  14968  cndcap  14969  dceqnconst  14970  dcapnconst  14971  nconstwlpolem0  14973  nconstwlpolem  14975  neap0mkv  14979  ltlenmkv  14980