Theorem r19.21bi 2407

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 2311	. . . 4 |- ( A. x e. A ps <-> A. x ( x e. A -> ps ) )
3	1, 2	sylib 127	. . 3 |- ( ph -> A. x ( x e. A -> ps ) )
4	3	19.21bi 1450	. 2 |- ( ph -> ( x e. A -> ps ) )
5	4	imp 115	1 |- ( ( ph /\ x e. A ) -> ps )

Syntax hints:   -> wi 4   /\ wa 97   A.wal 1241   e. wcel 1393   A.wral 2306

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-4 1400

This theorem depends on definitions:  df-bi 110  df-ral 2311

This theorem is referenced by:  rspec2  2408  rspec3  2409  r19.21be  2410  frind  4089  wepo  4096  wetrep  4097  ordelord  4118  ralxfr2d  4196  rexxfr2d  4197  funfveu  5188  f1oresrab  5329  isoselem  5459  tfrlemisucaccv  5939  prcdnql  6582  prcunqu  6583  prdisj  6590  caucvgsrlembound  6878  caucvgsrlemoffgt1  6883  monoord2  9236  caucvgrelemcau  9579  climrecvg1n  9867