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

Metamath Proof Explorer

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	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) → ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝜑 → 𝜑 )
2	1	ralrimivw	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝜑 )
3		r19.35	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 ) )
4	3	biimpi	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) → ( ∀ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 ) )
5	2 4	syl5	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) → ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 ) )