This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem r19.21be

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

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

Proof

Step Hyp Ref Expression
1 r19.21be.1 
 |-  ( ph -> A. x e. A ps )
2 1 r19.21bi 
 |-  ( ( ph /\ x e. A ) -> ps )
3 2 expcom 
 |-  ( x e. A -> ( ph -> ps ) )
4 3 rgen 
 |-  A. x e. A ( ph -> ps )