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

Metamath Proof Explorer

Theorem rexlimivw

Description: Weaker version of rexlimiv . (Contributed by FL, 19-Sep-2011) (Proof shortened by Wolf Lammen, 23-Dec-2024)

		Ref	Expression
	Hypothesis	rexlimivw.1	$⊢ φ \to ψ$
	Assertion	rexlimivw	$⊢ \exists x \in A φ \to ψ$

Step	Hyp	Ref	Expression
1		rexlimivw.1	$⊢ φ \to ψ$
2	1	adantl	$⊢ (x \in A \land φ) \to ψ$
3	2	rexlimiva	$⊢ \exists x \in A φ \to ψ$