Theorem rexlimi

Description: Restricted quantifier version of exlimi . (Contributed by NM, 30-Nov-2003) (Proof shortened by Andrew Salmon, 30-May-2011)

	Ref	Expression
Hypotheses	rexlimi.1	|- F/ x ps
	rexlimi.2	|- ( x e. A -> ( ph -> ps ) )
Assertion	rexlimi	|- ( E. x e. A ph -> ps )

Proof

Step	Hyp	Ref	Expression
1		rexlimi.1	|- F/ x ps
2		rexlimi.2	|- ( x e. A -> ( ph -> ps ) )
3	2	rgen	|- A. x e. A ( ph -> ps )
4	1	r19.23	|- ( A. x e. A ( ph -> ps ) <-> ( E. x e. A ph -> ps ) )
5	3 4	mpbi	|- ( E. x e. A ph -> ps )