Definition df-rn

Description: Define the range of a class. For example, F = { <. 2 , 6 >. , <. 3 , 9 >. } -> ran F = { 6 , 9 } ( ex-rn ). Contrast with domain (defined in df-dm ). For alternate definitions, see dfrn2 , dfrn3 , and dfrn4 . The notation " ran " is used by Enderton. The range of a function is often also called "the image of the function" (see definition in Lang p. ix), which can be justified by imadmrn . Not to be confused with "codomain" (see df-f ), which may be a superset/superclass of the range (see frn ). (Contributed by NM, 1-Aug-1994)

	Ref	Expression
Assertion	df-rn	$$⊢\mathrm{ran}A=\mathrm{dom}{A}^{-1}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	crn	$$class\mathrm{ran}A$$
2	0	ccnv	$$class{A}^{-1}$$
3	2	cdm	$$class\mathrm{dom}{A}^{-1}$$
4	1 3	wceq	$$wff\mathrm{ran}A=\mathrm{dom}{A}^{-1}$$