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	|- F/ x ph
	rnmpt0f.2	|- ( ( ph /\ x e. A ) -> B e. V )
	rnmpt0f.3	|- F = ( x e. A |-> B )
	rnmptn0.a	|- ( ph -> A =/= (/) )
Assertion	rnmptn0	|- ( ph -> ran F =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		rnmpt0f.1	|- F/ x ph
2		rnmpt0f.2	|- ( ( ph /\ x e. A ) -> B e. V )
3		rnmpt0f.3	|- F = ( x e. A |-> B )
4		rnmptn0.a	|- ( ph -> A =/= (/) )
5	4	neneqd	|- ( ph -> -. A = (/) )
6	1 2 3	rnmpt0f	|- ( ph -> ( ran F = (/) <-> A = (/) ) )
7	5 6	mtbird	|- ( ph -> -. ran F = (/) )
8	7	neqned	|- ( ph -> ran F =/= (/) )