Theorem r19.21bi 2462

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 2365	. . . 4 |- ( A. x e. A ps <-> A. x ( x e. A -> ps ) )
3	1, 2	sylib 121	. . 3 |- ( ph -> A. x ( x e. A -> ps ) )
4	3	19.21bi 1496	. 2 |- ( ph -> ( x e. A -> ps ) )
5	4	imp 123	1 |- ( ( ph /\ x e. A ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103   A.wal 1288   e. wcel 1439   A.wral 2360

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

This theorem depends on definitions:  df-bi 116  df-ral 2365

This theorem is referenced by:  rspec2  2463  rspec3  2464  r19.21be  2465  frind  4188  wepo  4195  wetrep  4196  ordelord  4217  ralxfr2d  4299  rexxfr2d  4300  funfveu  5331  f1oresrab  5477  isoselem  5613  disjxp1  6015  tfrlemisucaccv  6104  tfr1onlemsucaccv  6120  tfrcllemsucaccv  6133  xpf1o  6614  fimax2gtrilemstep  6670  supisoti  6759  exmidomni  6852  prcdnql  7097  prcunqu  7098  prdisj  7105  caucvgsrlembound  7393  caucvgsrlemoffgt1  7398  exbtwnzlemex  9715  monoord2  9959  iseqf1olemqk  9977  seq3f1olemqsumk  9982  caucvgrelemcau  10467  fimaxre2  10712  climrecvg1n  10791  zisum  10828  fisum  10832  isumss2  10839  fisumser  10844  sumpr  10861  sumtp  10862  fsum2dlemstep  10882  fsumiun  10925  isumlessdc  10944  bezoutlemstep  11318