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	$$⊢Ⅎx\phi$$
	rnmpt0f.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
	rnmpt0f.3	$$⊢F=\left(x\in A⟼B\right)$$
	rnmptn0.a	$$⊢\phi \to A\ne \varnothing$$
Assertion	rnmptn0	$$⊢\phi \to \mathrm{ran}F\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		rnmpt0f.1	$$⊢Ⅎx\phi$$
2		rnmpt0f.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
3		rnmpt0f.3	$$⊢F=\left(x\in A⟼B\right)$$
4		rnmptn0.a	$$⊢\phi \to A\ne \varnothing$$
5	4	neneqd	$$⊢\phi \to \neg A=\varnothing$$
6	1 2 3	rnmpt0f	$$⊢\phi \to \left(\mathrm{ran}F=\varnothing \leftrightarrow A=\varnothing \right)$$
7	5 6	mtbird	$$⊢\phi \to \neg \mathrm{ran}F=\varnothing$$
8	7	neqned	$$⊢\phi \to \mathrm{ran}F\ne \varnothing$$