Definition df-rn 5639

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 30507). Contrast with domain (defined in df-dm 5638). For alternate definitions, see dfrn2 5841, dfrn3 5842, and dfrn4 6164. 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 6033. Not to be confused with "codomain" (see df-f 6500), which may be a superset/superclass of the range (see frn 6673). (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-rn	⊢ ran 𝐴 = dom ◡𝐴

Detailed syntax breakdown of Definition df-rn

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	crn 5629	. 2 class ran 𝐴
3	1	ccnv 5627	. . 3 class ◡𝐴
4	3	cdm 5628	. 2 class dom ◡𝐴
5	2, 4	wceq 1542	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5841  dmcnvcnv  5886  rncnvcnv  5887  rneq  5889  rnss  5892  brelrng  5894  nfrn  5905  rncoss  5930  rncoeq  5935  cnvimarndm  6046  rnun  6107  rnin  6108  rnxp  6132  rnxpss  6134  imainrect  6143  rnsnopg  6183  cnvssrndm  6233  unidmrn  6241  dfdm2  6243  funcnvpr  6558  funcnvtp  6559  funcnvqp  6560  fncnv  6569  funcnvres  6574  funimacnv  6577  fimacnvdisj  6716  dff1o4  6786  foimacnv  6795  funcocnv2  6803  f1ompt  7061  nvof1o  7232  cnvexg  7872  tz7.48-3  8380  errn  8663  omxpenlem  9013  sbthlem5  9026  sbthlem8  9029  sbthlem9  9030  fodomr  9063  domss2  9071  fodomfir  9235  rnfi  9247  zorn2lem4  10418  rnct  10444  fpwwe2lem12  10562  trclublem  14954  relexpcnv  14994  relexpnnrn  15004  invf  17732  cicsym  17768  cnvtsr  18551  znleval  21531  ordtbas2  23153  ordtcnv  23163  ordtrest2  23166  cnconn  23384  tgqtop  23674  adj1o  31962  fcoinver  32671  fresf1o  32701  fcnvgreu  32742  dfcnv2  32745  preiman0  32780  gsumhashmul  33125  cycpmfvlem  33170  cycpmfv1  33171  cycpmfv2  33172  cycpmfv3  33173  cycpmrn  33201  cnvordtrestixx  34054  xrge0iifhmeo  34077  mbfmcst  34400  0rrv  34592  elrn3  35941  dfrn6  38626  cnvresrn  38666  dmxrn  38705  dmcoss2  38862  cnvrcl0  44049  conrel2d  44088  relexpaddss  44142  rntrclfvRP  44155  ntrneifv2  44504