Theorem imadmrn

Description: The image of the domain of a class is equal to its range. (Contributed by NM, 14-Aug-1994) (Proof shortened by BJ, 27-Sep-2026)

	Ref	Expression
Assertion	imadmrn	⊢ ( 𝐴 “ dom 𝐴 ) = ran 𝐴

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ dom 𝐴 ⊆ dom 𝐴
2		dfrn7	⊢ ( dom 𝐴 ⊆ dom 𝐴 → ran 𝐴 = ( 𝐴 “ dom 𝐴 ) )
3	2	eqcomd	⊢ ( dom 𝐴 ⊆ dom 𝐴 → ( 𝐴 “ dom 𝐴 ) = ran 𝐴 )
4	1 3	ax-mp	⊢ ( 𝐴 “ dom 𝐴 ) = ran 𝐴