Theorem r19.21bi 2618

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.)

Hypothesis

Ref	Expression
r19.21bi.1	|- ( ph -> A. x e. A ps )

Assertion

Ref	Expression
r19.21bi	|- ( ( ph /\ x e. A ) -> ps )

Proof of Theorem r19.21bi

Step	Hyp	Ref	Expression
1		r19.21bi.1	. . . 4 |- ( ph -> A. x e. A ps )
2		df-ral 2513	. . . 4 |- ( A. x e. A ps <-> A. x ( x e. A -> ps ) )
3	1, 2	sylib 122	. . 3 |- ( ph -> A. x ( x e. A -> ps ) )
4	3	19.21bi 1604	. 2 |- ( ph -> ( x e. A -> ps ) )
5	4	imp 124	1 |- ( ( ph /\ x e. A ) -> ps )

Syntax hints:   -> wi 4   /\ wa 104   A.wal 1393   e. wcel 2200   A.wral 2508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-4 1556

This theorem depends on definitions:  df-bi 117  df-ral 2513

This theorem is referenced by:  rspec2  2619  rspec3  2620  r19.21be  2621  frind  4443  wepo  4450  wetrep  4451  ordelord  4472  ralxfr2d  4555  rexxfr2d  4556  funfveu  5640  fvmptelcdm  5788  f1oresrab  5800  isoselem  5944  mpoexw  6359  disjxp1  6382  tfrlemisucaccv  6471  tfr1onlemsucaccv  6487  tfrcllemsucaccv  6500  xpf1o  7005  fimax2gtrilemstep  7062  supisoti  7177  difinfsn  7267  exmidomni  7309  cc3  7454  prcdnql  7671  prcunqu  7672  prdisj  7679  caucvgsrlembound  7981  caucvgsrlemoffgt1  7986  exbtwnzlemex  10469  monoord2  10708  iseqf1olemqk  10729  seq3f1olemqsumk  10734  caucvgrelemcau  11491  fimaxre2  11738  climrecvg1n  11859  zsumdc  11895  fsum3  11898  isumss2  11904  fsum3ser  11908  sumpr  11924  sumtp  11925  fsum2dlemstep  11945  fsumiun  11988  isumlessdc  12007  zproddc  12090  fprodsplitdc  12107  fprodcl2lem  12116  fprod2dlemstep  12133  bezoutlemstep  12518  ennnfonelemim  12995  ctiunctal  13012  prdsmndd  13481  grppropd  13550  srgdilem  13932  srgrz  13947  srglz  13948  cnmpt11  14957  psmet0  15001  psmettri2  15002  mulcncflem  15281  mulcncf  15282  dedekindeulemuub  15291  dedekindeulemlu  15295  dedekindicclemuub  15300  dedekindicclemlu  15304  limccnpcntop  15349  limccnp2lem  15350  limccnp2cntop  15351  plycoeid3  15431  fsumdvdsmul  15665  bj-charfundc  16171  bj-charfunbi  16174  nninffeq  16386  refeq  16396  iswomni0  16419  nconstwlpolem  16433