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

Metamath Proof Explorer

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 ) )