Theorem wnefimgd

Description: The image of a mapping from A is nonempty if A is nonempty. (Contributed by Stanislas Polu, 9-Mar-2020)

	Ref	Expression
Hypotheses	wnefimgd.1	$$⊢\phi \to A\ne \varnothing$$
	wnefimgd.2	$$⊢\phi \to F:A⟶B$$
Assertion	wnefimgd	$$⊢\phi \to F\left[A\right]\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		wnefimgd.1	$$⊢\phi \to A\ne \varnothing$$
2		wnefimgd.2	$$⊢\phi \to F:A⟶B$$
3		ssid	$$⊢A\subseteq A$$
4	2	fdmd	$$⊢\phi \to \mathrm{dom}F=A$$
5	3 4	sseqtrrid	$$⊢\phi \to A\subseteq \mathrm{dom}F$$
6		sseqin2	$$⊢A\subseteq \mathrm{dom}F\leftrightarrow \mathrm{dom}F\cap A=A$$
7	5 6	sylib	$$⊢\phi \to \mathrm{dom}F\cap A=A$$
8	7 1	eqnetrd	$$⊢\phi \to \mathrm{dom}F\cap A\ne \varnothing$$
9	8	imadisjlnd	$$⊢\phi \to F\left[A\right]\ne \varnothing$$