Definition df-rn 5633

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 30464). Contrast with domain (defined in df-dm 5632). For alternate definitions, see dfrn2 5835, dfrn3 5836, and dfrn4 6158. 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 6027. Not to be confused with "codomain" (see df-f 6494), which may be a superset/superclass of the range (see frn 6667). (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 5623	. 2 class ran 𝐴
3	1	ccnv 5621	. . 3 class ◡𝐴
4	3	cdm 5622	. 2 class dom ◡𝐴
5	2, 4	wceq 1541	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5835  dmcnvcnv  5880  rncnvcnv  5881  rneq  5883  rnss  5886  brelrng  5888  nfrn  5899  rncoss  5924  rncoeq  5929  cnvimarndm  6040  rnun  6101  rnin  6102  rnxp  6126  rnxpss  6128  imainrect  6137  rnsnopg  6177  cnvssrndm  6227  unidmrn  6235  dfdm2  6237  funcnvpr  6552  funcnvtp  6553  funcnvqp  6554  fncnv  6563  funcnvres  6568  funimacnv  6571  fimacnvdisj  6710  dff1o4  6780  foimacnv  6789  funcocnv2  6797  f1ompt  7054  nvof1o  7224  cnvexg  7864  tz7.48-3  8373  errn  8655  omxpenlem  9004  sbthlem5  9017  sbthlem8  9020  sbthlem9  9021  fodomr  9054  domss2  9062  fodomfir  9226  rnfi  9238  zorn2lem4  10407  rnct  10433  fpwwe2lem12  10551  trclublem  14916  relexpcnv  14956  relexpnnrn  14966  invf  17690  cicsym  17726  cnvtsr  18509  znleval  21507  ordtbas2  23133  ordtcnv  23143  ordtrest2  23146  cnconn  23364  tgqtop  23654  adj1o  31918  fcoinver  32628  fresf1o  32658  fcnvgreu  32700  dfcnv2  32703  preiman0  32738  gsumhashmul  33099  cycpmfvlem  33143  cycpmfv1  33144  cycpmfv2  33145  cycpmfv3  33146  cycpmrn  33174  cnvordtrestixx  34019  xrge0iifhmeo  34042  mbfmcst  34365  0rrv  34557  elrn3  35905  dfrn6  38440  cnvresrn  38480  dmxrn  38511  dmcoss2  38656  cnvrcl0  43808  conrel2d  43847  relexpaddss  43901  rntrclfvRP  43914  ntrneifv2  44263