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 " ( dom F \ A ) ) C_ ran ( F |` A ) -> ran F = ran ( F |` A ) )

Proof

Step	Hyp	Ref	Expression
1		ssid	|- ( dom F \ A ) C_ ( dom F \ A )
2		ssundif	|- ( dom F C_ ( A u. ( dom F \ A ) ) <-> ( dom F \ A ) C_ ( dom F \ A ) )
3	1 2	mpbir	|- dom F C_ ( A u. ( dom F \ A ) )
4		dfrn7	|- ( dom F C_ ( A u. ( dom F \ A ) ) -> ran F = ( F " ( A u. ( dom F \ A ) ) ) )
5	3 4	ax-mp	|- ran F = ( F " ( A u. ( dom F \ A ) ) )
6		imaundi	|- ( F " ( A u. ( dom F \ A ) ) ) = ( ( F " A ) u. ( F " ( dom F \ A ) ) )
7	5 6	eqtri	|- ran F = ( ( F " A ) u. ( F " ( dom F \ A ) ) )
8		df-ima	|- ( F " A ) = ran ( F |` A )
9	8	sseq2i	|- ( ( F " ( dom F \ A ) ) C_ ( F " A ) <-> ( F " ( dom F \ A ) ) C_ ran ( F |` A ) )
10		ssequn2	|- ( ( F " ( dom F \ A ) ) C_ ( F " A ) <-> ( ( F " A ) u. ( F " ( dom F \ A ) ) ) = ( F " A ) )
11	9 10	sylbb1	|- ( ( F " ( dom F \ A ) ) C_ ran ( F |` A ) -> ( ( F " A ) u. ( F " ( dom F \ A ) ) ) = ( F " A ) )
12	7 11	eqtrid	|- ( ( F " ( dom F \ A ) ) C_ ran ( F |` A ) -> ran F = ( F " A ) )
13	12 8	eqtrdi	|- ( ( F " ( dom F \ A ) ) C_ ran ( F |` A ) -> ran F = ran ( F |` A ) )