Definition df-rn 5269

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 27600). Contrast with domain (defined in df-dm 5268). For alternate definitions, see dfrn2 5458, dfrn3 5459, and dfrn4 5745. The notation "ran " is used by Enderton; other authors sometimes use script R or script W. (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 5259	. 2 class ran 𝐴
3	1	ccnv 5257	. . 3 class ◡𝐴
4	3	cdm 5258	. 2 class dom ◡𝐴
5	2, 4	wceq 1624	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5458  dmcnvcnv  5495  rncnvcnv  5496  rneq  5498  rnss  5501  brelrng  5502  nfrn  5515  rncoss  5533  rncoeq  5536  cnvimarndm  5636  rnun  5691  rnin  5692  rnxp  5714  rnxpss  5716  imainrect  5725  rnsnopg  5765  cnvssrndm  5810  unidmrn  5818  dfdm2  5820  funcnvpr  6103  funcnvtp  6104  funcnvqp  6105  funcnvqpOLD  6106  fncnv  6115  funcnvres  6120  funimacnv  6123  fimacnvdisj  6236  dff1o4  6298  foimacnv  6307  funcocnv2  6314  f1ompt  6537  nvof1o  6691  cnvexg  7269  tz7.48-3  7700  errn  7925  omxpenlem  8218  sbthlem5  8231  sbthlem8  8234  sbthlem9  8235  fodomr  8268  domss2  8276  rnfi  8406  zorn2lem4  9505  rnct  9531  fpwwe2lem13  9648  trclublem  13927  relexpcnv  13966  relexpnnrn  13976  invf  16621  cicsym  16657  cnvtsr  17415  znleval  20097  ordtbas2  21189  ordtcnv  21199  ordtrest2  21202  cnconn  21419  tgqtop  21709  adj1o  29054  fcoinver  29717  fresf1o  29734  fcnvgreu  29773  dfcnv2  29777  cnvordtrestixx  30260  xrge0iifhmeo  30283  mbfmcst  30622  0rrv  30814  elrn3  31951  dfrn6  34388  cnvresrn  34431  dmcoss2  34519  cnvrcl0  38426  conrel2d  38450  relexpaddss  38504  rntrclfvRP  38517  ntrneifv2  38872