Theorem r19.37v

Description: Restricted quantifier version of one direction of 19.37v . (The other direction holds iff A is nonempty, see r19.37zv .) (Contributed by NM, 2-Apr-2004) Reduce axiom usage. (Revised by Wolf Lammen, 18-Jun-2023)

	Ref	Expression
Assertion	r19.37v	|- ( E. x e. A ( ph -> ps ) -> ( ph -> E. x e. A ps ) )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( ph -> ph )
2	1	ralrimivw	|- ( ph -> A. x e. A ph )
3		r19.35	|- ( E. x e. A ( ph -> ps ) <-> ( A. x e. A ph -> E. x e. A ps ) )
4	3	biimpi	|- ( E. x e. A ( ph -> ps ) -> ( A. x e. A ph -> E. x e. A ps ) )
5	2 4	syl5	|- ( E. x e. A ( ph -> ps ) -> ( ph -> E. x e. A ps ) )