Theorem imadifssrn

Description: Condition for the range of a class to be the range of one of its restrictions. (Contributed by AV, 4-Oct-2025) Remove antecedent. (Revised by Eric Schmidt, 10-Jul-2026) (Proof shortened by BJ, 29-Sep-2026)

	Ref	Expression
Assertion	imadifssrn	$$⊢F\left[\mathrm{dom}F\setminus A\right]\subseteq \mathrm{ran}\left({F\upharpoonright }_A\right)\to \mathrm{ran}F=\mathrm{ran}\left({F\upharpoonright }_A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssid	$$⊢\mathrm{dom}F\setminus A\subseteq \mathrm{dom}F\setminus A$$
2		ssundif	$$⊢\mathrm{dom}F\subseteq A\cup \left(\mathrm{dom}F\setminus A\right)\leftrightarrow \mathrm{dom}F\setminus A\subseteq \mathrm{dom}F\setminus A$$
3	1 2	mpbir	$$⊢\mathrm{dom}F\subseteq A\cup \left(\mathrm{dom}F\setminus A\right)$$
4		dfrn7	$$⊢\mathrm{dom}F\subseteq A\cup \left(\mathrm{dom}F\setminus A\right)\to \mathrm{ran}F=F\left[A\cup \left(\mathrm{dom}F\setminus A\right)\right]$$
5	3 4	ax-mp	$$⊢\mathrm{ran}F=F\left[A\cup \left(\mathrm{dom}F\setminus A\right)\right]$$
6		imaundi	$$⊢F\left[A\cup \left(\mathrm{dom}F\setminus A\right)\right]=F\left[A\right]\cup F\left[\mathrm{dom}F\setminus A\right]$$
7	5 6	eqtri	$$⊢\mathrm{ran}F=F\left[A\right]\cup F\left[\mathrm{dom}F\setminus A\right]$$
8		df-ima	$$⊢F\left[A\right]=\mathrm{ran}\left({F\upharpoonright }_A\right)$$
9	8	sseq2i	$$⊢F\left[\mathrm{dom}F\setminus A\right]\subseteq F\left[A\right]\leftrightarrow F\left[\mathrm{dom}F\setminus A\right]\subseteq \mathrm{ran}\left({F\upharpoonright }_A\right)$$
10		ssequn2	$$⊢F\left[\mathrm{dom}F\setminus A\right]\subseteq F\left[A\right]\leftrightarrow F\left[A\right]\cup F\left[\mathrm{dom}F\setminus A\right]=F\left[A\right]$$
11	9 10	sylbb1	$$⊢F\left[\mathrm{dom}F\setminus A\right]\subseteq \mathrm{ran}\left({F\upharpoonright }_A\right)\to F\left[A\right]\cup F\left[\mathrm{dom}F\setminus A\right]=F\left[A\right]$$
12	7 11	eqtrid	$$⊢F\left[\mathrm{dom}F\setminus A\right]\subseteq \mathrm{ran}\left({F\upharpoonright }_A\right)\to \mathrm{ran}F=F\left[A\right]$$
13	12 8	eqtrdi	$$⊢F\left[\mathrm{dom}F\setminus A\right]\subseteq \mathrm{ran}\left({F\upharpoonright }_A\right)\to \mathrm{ran}F=\mathrm{ran}\left({F\upharpoonright }_A\right)$$