Definition df-rn 5631

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 30498). Contrast with domain (defined in df-dm 5630). For alternate definitions, see dfrn2 5832, dfrn3 5833, and dfrn4 6155. 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 6024. Not to be confused with "codomain" (see df-f 6491), which may be a superset/superclass of the range (see frn 6664). (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 5621	. 2 class ran 𝐴
3	1	ccnv 5619	. . 3 class ◡𝐴
4	3	cdm 5620	. 2 class dom ◡𝐴
5	2, 4	wceq 1542	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5832  dmcnvcnv  5877  rncnvcnv  5878  rneq  5880  rnss  5883  brelrng  5885  nfrn  5896  rncoss  5921  rncoeq  5926  cnvimarndm  6037  rnun  6098  rnin  6099  rnxp  6123  rnxpss  6125  imainrect  6134  rnsnopg  6174  cnvssrndm  6224  unidmrn  6232  dfdm2  6234  funcnvpr  6549  funcnvtp  6550  funcnvqp  6551  fncnv  6560  funcnvres  6565  funimacnv  6568  fimacnvdisj  6707  dff1o4  6777  foimacnv  6786  funcocnv2  6794  f1ompt  7052  nvof1o  7224  cnvexg  7864  tz7.48-3  8372  errn  8655  omxpenlem  9005  sbthlem5  9018  sbthlem8  9021  sbthlem9  9022  fodomr  9055  domss2  9063  fodomfir  9227  rnfi  9239  zorn2lem4  10410  rnct  10436  fpwwe2lem12  10554  trclublem  14946  relexpcnv  14986  relexpnnrn  14996  invf  17724  cicsym  17760  cnvtsr  18543  znleval  21523  ordtbas2  23144  ordtcnv  23154  ordtrest2  23157  cnconn  23375  tgqtop  23665  adj1o  31953  fcoinver  32662  fresf1o  32692  fcnvgreu  32733  dfcnv2  32736  preiman0  32771  gsumhashmul  33116  cycpmfvlem  33161  cycpmfv1  33162  cycpmfv2  33163  cycpmfv3  33164  cycpmrn  33192  cnvordtrestixx  34045  xrge0iifhmeo  34068  mbfmcst  34391  0rrv  34583  elrn3  35932  dfrn6  38617  cnvresrn  38657  dmxrn  38696  dmcoss2  38853  cnvrcl0  44040  conrel2d  44079  relexpaddss  44133  rntrclfvRP  44146  ntrneifv2  44495