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

Metamath Proof Explorer

Theorem rexlimi

Description: Restricted quantifier version of exlimi . For a version based on fewer axioms see rexlimiv . (Contributed by NM, 30-Nov-2003) (Proof shortened by Andrew Salmon, 30-May-2011)

	Ref	Expression
Hypotheses	rexlimi.1	$⊢ Ⅎ x ψ$
	rexlimi.2	$⊢ x \in A \to (φ \to ψ)$
Assertion	rexlimi	$⊢ \exists x \in A φ \to ψ$

Proof

Step	Hyp	Ref	Expression
1		rexlimi.1	$⊢ Ⅎ x ψ$
2		rexlimi.2	$⊢ x \in A \to (φ \to ψ)$
3	2	rgen	$⊢ \forall x \in A (φ \to ψ)$
4	1	r19.23	$⊢ \forall x \in A (φ \to ψ) \leftrightarrow (\exists x \in A φ \to ψ)$
5	3 4	mpbi	$⊢ \exists x \in A φ \to ψ$