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	⊢ ( ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) → ran 𝐹 = ran ( 𝐹 ↾ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ ( dom 𝐹 ∖ 𝐴 ) ⊆ ( dom 𝐹 ∖ 𝐴 )
2		ssundif	⊢ ( dom 𝐹 ⊆ ( 𝐴 ∪ ( dom 𝐹 ∖ 𝐴 ) ) ↔ ( dom 𝐹 ∖ 𝐴 ) ⊆ ( dom 𝐹 ∖ 𝐴 ) )
3	1 2	mpbir	⊢ dom 𝐹 ⊆ ( 𝐴 ∪ ( dom 𝐹 ∖ 𝐴 ) )
4		dfrn7	⊢ ( dom 𝐹 ⊆ ( 𝐴 ∪ ( dom 𝐹 ∖ 𝐴 ) ) → ran 𝐹 = ( 𝐹 “ ( 𝐴 ∪ ( dom 𝐹 ∖ 𝐴 ) ) ) )
5	3 4	ax-mp	⊢ ran 𝐹 = ( 𝐹 “ ( 𝐴 ∪ ( dom 𝐹 ∖ 𝐴 ) ) )
6		imaundi	⊢ ( 𝐹 “ ( 𝐴 ∪ ( dom 𝐹 ∖ 𝐴 ) ) ) = ( ( 𝐹 “ 𝐴 ) ∪ ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) )
7	5 6	eqtri	⊢ ran 𝐹 = ( ( 𝐹 “ 𝐴 ) ∪ ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) )
8		df-ima	⊢ ( 𝐹 “ 𝐴 ) = ran ( 𝐹 ↾ 𝐴 )
9	8	sseq2i	⊢ ( ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ( 𝐹 “ 𝐴 ) ↔ ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) )
10		ssequn2	⊢ ( ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ( 𝐹 “ 𝐴 ) ↔ ( ( 𝐹 “ 𝐴 ) ∪ ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) ) = ( 𝐹 “ 𝐴 ) )
11	9 10	sylbb1	⊢ ( ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) → ( ( 𝐹 “ 𝐴 ) ∪ ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) ) = ( 𝐹 “ 𝐴 ) )
12	7 11	eqtrid	⊢ ( ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) → ran 𝐹 = ( 𝐹 “ 𝐴 ) )
13	12 8	eqtrdi	⊢ ( ( 𝐹 “ ( dom 𝐹 ∖ 𝐴 ) ) ⊆ ran ( 𝐹 ↾ 𝐴 ) → ran 𝐹 = ran ( 𝐹 ↾ 𝐴 ) )