Theorem r19.21bi 2449

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 2353	. . . 4 |- ( A. x e. A ps <-> A. x ( x e. A -> ps ) )
3	1, 2	sylib 120	. . 3 |- ( ph -> A. x ( x e. A -> ps ) )
4	3	19.21bi 1490	. 2 |- ( ph -> ( x e. A -> ps ) )
5	4	imp 122	1 |- ( ( ph /\ x e. A ) -> ps )

Syntax hints:   -> wi 4   /\ wa 102   A.wal 1282   e. wcel 1433   A.wral 2348

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

This theorem depends on definitions:  df-bi 115  df-ral 2353

This theorem is referenced by:  rspec2  2450  rspec3  2451  r19.21be  2452  frind  4107  wepo  4114  wetrep  4115  ordelord  4136  ralxfr2d  4214  rexxfr2d  4215  funfveu  5208  f1oresrab  5350  isoselem  5479  tfrlemisucaccv  5962  supisoti  6423  prcdnql  6674  prcunqu  6675  prdisj  6682  caucvgsrlembound  6970  caucvgsrlemoffgt1  6975  monoord2  9456  caucvgrelemcau  9866  fimaxre2  10109  climrecvg1n  10185  bezoutlemstep  10386