Definition df-rn 5566

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 28219). Contrast with domain (defined in df-dm 5565). For alternate definitions, see dfrn2 5759, dfrn3 5760, and dfrn4 6059. 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 5939. Not to be confused with "codomain" (see df-f 6359), which may be a superset/superclass of the range (see frn 6520). (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 5556	. 2 class ran 𝐴
3	1	ccnv 5554	. . 3 class ◡𝐴
4	3	cdm 5555	. 2 class dom ◡𝐴
5	2, 4	wceq 1537	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5759  dmcnvcnv  5803  rncnvcnv  5804  rneq  5806  rnss  5809  brelrng  5811  nfrn  5824  rncoss  5843  rncoeq  5846  cnvimarndm  5950  rnun  6004  rnin  6005  rnxp  6027  rnxpss  6029  imainrect  6038  rnsnopg  6078  cnvssrndm  6122  unidmrn  6130  dfdm2  6132  funcnvpr  6416  funcnvtp  6417  funcnvqp  6418  fncnv  6427  funcnvres  6432  funimacnv  6435  fimacnvdisj  6557  dff1o4  6623  foimacnv  6632  funcocnv2  6639  f1ompt  6875  nvof1o  7037  cnvexg  7629  tz7.48-3  8080  errn  8311  omxpenlem  8618  sbthlem5  8631  sbthlem8  8634  sbthlem9  8635  fodomr  8668  domss2  8676  rnfi  8807  zorn2lem4  9921  rnct  9947  fpwwe2lem13  10064  trclublem  14355  relexpcnv  14394  relexpnnrn  14404  invf  17038  cicsym  17074  cnvtsr  17832  znleval  20701  ordtbas2  21799  ordtcnv  21809  ordtrest2  21812  cnconn  22030  tgqtop  22320  adj1o  29671  fcoinver  30357  fresf1o  30376  fcnvgreu  30418  dfcnv2  30422  cycpmfvlem  30754  cycpmfv1  30755  cycpmfv2  30756  cycpmfv3  30757  cycpmrn  30785  cnvordtrestixx  31156  xrge0iifhmeo  31179  mbfmcst  31517  0rrv  31709  elrn3  32998  dfrn6  35575  cnvresrn  35620  dmcoss2  35709  cnvrcl0  40034  conrel2d  40058  relexpaddss  40112  rntrclfvRP  40125  ntrneifv2  40479