Definition df-rn 5530

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 28225). Contrast with domain (defined in df-dm 5529). For alternate definitions, see dfrn2 5723, dfrn3 5724, and dfrn4 6026. 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 5906. Not to be confused with "codomain" (see df-f 6328), which may be a superset/superclass of the range (see frn 6493). (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 5520	. 2 class ran 𝐴
3	1	ccnv 5518	. . 3 class ◡𝐴
4	3	cdm 5519	. 2 class dom ◡𝐴
5	2, 4	wceq 1538	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5723  dmcnvcnv  5767  rncnvcnv  5768  rneq  5770  rnss  5773  brelrng  5775  nfrn  5788  rncoss  5808  rncoeq  5811  cnvimarndm  5917  rnun  5971  rnin  5972  rnxp  5994  rnxpss  5996  imainrect  6005  rnsnopg  6045  cnvssrndm  6090  unidmrn  6098  dfdm2  6100  funcnvpr  6386  funcnvtp  6387  funcnvqp  6388  fncnv  6397  funcnvres  6402  funimacnv  6405  fimacnvdisj  6531  dff1o4  6598  foimacnv  6607  funcocnv2  6614  f1ompt  6852  nvof1o  7015  cnvexg  7611  tz7.48-3  8063  errn  8294  omxpenlem  8601  sbthlem5  8615  sbthlem8  8618  sbthlem9  8619  fodomr  8652  domss2  8660  rnfi  8791  zorn2lem4  9910  rnct  9936  fpwwe2lem13  10053  trclublem  14346  relexpcnv  14386  relexpnnrn  14396  invf  17030  cicsym  17066  cnvtsr  17824  znleval  20246  ordtbas2  21796  ordtcnv  21806  ordtrest2  21809  cnconn  22027  tgqtop  22317  adj1o  29677  fcoinver  30370  fresf1o  30390  fcnvgreu  30436  dfcnv2  30439  preiman0  30469  gsumhashmul  30741  cycpmfvlem  30804  cycpmfv1  30805  cycpmfv2  30806  cycpmfv3  30807  cycpmrn  30835  cnvordtrestixx  31266  xrge0iifhmeo  31289  mbfmcst  31627  0rrv  31819  elrn3  33111  dfrn6  35720  cnvresrn  35765  dmcoss2  35854  cnvrcl0  40325  conrel2d  40365  relexpaddss  40419  rntrclfvRP  40432  ntrneifv2  40783