Theorem rnmptn0

Description: The range of a function in maps-to notation is nonempty if the domain is nonempty. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	rnmpt0f.1	⊢ Ⅎ 𝑥 𝜑
	rnmpt0f.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
	rnmpt0f.3	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	rnmptn0.a	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
Assertion	rnmptn0	⊢ ( 𝜑 → ran 𝐹 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		rnmpt0f.1	⊢ Ⅎ 𝑥 𝜑
2		rnmpt0f.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
3		rnmpt0f.3	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
4		rnmptn0.a	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
5	4	neneqd	⊢ ( 𝜑 → ¬ 𝐴 = ∅ )
6	1 2 3	rnmpt0f	⊢ ( 𝜑 → ( ran 𝐹 = ∅ ↔ 𝐴 = ∅ ) )
7	5 6	mtbird	⊢ ( 𝜑 → ¬ ran 𝐹 = ∅ )
8	7	neqned	⊢ ( 𝜑 → ran 𝐹 ≠ ∅ )