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	$$⊢\exists x\in A\left(\phi \to \psi \right)\to \left(\phi \to \exists x\in A\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢\phi \to \phi$$
2	1	ralrimivw	$$⊢\phi \to \forall x\in A\phi$$
3		r19.35	$$⊢\exists x\in A\left(\phi \to \psi \right)\leftrightarrow \left(\forall x\in A\phi \to \exists x\in A\psi \right)$$
4	3	biimpi	$$⊢\exists x\in A\left(\phi \to \psi \right)\to \left(\forall x\in A\phi \to \exists x\in A\psi \right)$$
5	2 4	syl5	$$⊢\exists x\in A\left(\phi \to \psi \right)\to \left(\phi \to \exists x\in A\psi \right)$$