Metamath Proof Explorer


Theorem rexlimivw

Description: Weaker version of rexlimiv . (Contributed by FL, 19-Sep-2011)

Ref Expression
Hypothesis rexlimivw.1
|- ( ph -> ps )
Assertion rexlimivw
|- ( E. x e. A ph -> ps )

Proof

Step Hyp Ref Expression
1 rexlimivw.1
 |-  ( ph -> ps )
2 1 a1i
 |-  ( x e. A -> ( ph -> ps ) )
3 2 rexlimiv
 |-  ( E. x e. A ph -> ps )