Theorem r19.37

Description: Restricted quantifier version of one direction of 19.37 . (The other direction does not hold when A is empty.) (Contributed by FL, 13-May-2012) (Revised by Mario Carneiro, 11-Dec-2016)

	Ref	Expression
Hypothesis	r19.37.1	|- F/ x ph
Assertion	r19.37	|- ( E. x e. A ( ph -> ps ) -> ( ph -> E. x e. A ps ) )

Proof

Step	Hyp	Ref	Expression
1		r19.37.1	|- F/ x ph
2		r19.35	|- ( E. x e. A ( ph -> ps ) <-> ( A. x e. A ph -> E. x e. A ps ) )
3		ax-1	|- ( ph -> ( x e. A -> ph ) )
4	1 3	ralrimi	|- ( ph -> A. x e. A ph )
5	4	imim1i	|- ( ( A. x e. A ph -> E. x e. A ps ) -> ( ph -> E. x e. A ps ) )
6	2 5	sylbi	|- ( E. x e. A ( ph -> ps ) -> ( ph -> E. x e. A ps ) )