Definition df-rn 5154

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 27427). Contrast with domain (defined in df-dm 5153). For alternate definitions, see dfrn2 5343, dfrn3 5344, and dfrn4 5630. 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 5144	. 2 class ran 𝐴
3	1	ccnv 5142	. . 3 class ◡𝐴
4	3	cdm 5143	. 2 class dom ◡𝐴
5	2, 4	wceq 1523	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5343  dmcnvcnv  5380  rncnvcnv  5381  rneq  5383  rnss  5386  brelrng  5387  nfrn  5400  rncoss  5418  rncoeq  5421  cnvimarndm  5521  rnun  5576  rnin  5577  rnxp  5599  rnxpss  5601  imainrect  5610  rnsnopg  5650  cnvssrndm  5695  unidmrn  5703  dfdm2  5705  funcnvpr  5988  funcnvtp  5989  funcnvqp  5990  funcnvqpOLD  5991  fncnv  6000  funcnvres  6005  funimacnv  6008  fimacnvdisj  6121  dff1o4  6183  foimacnv  6192  funcocnv2  6199  f1ompt  6422  nvof1o  6576  cnvexg  7154  tz7.48-3  7584  errn  7809  omxpenlem  8102  sbthlem5  8115  sbthlem8  8118  sbthlem9  8119  fodomr  8152  domss2  8160  rnfi  8290  zorn2lem4  9359  rnct  9385  fpwwe2lem13  9502  trclublem  13780  relexpcnv  13819  relexpnnrn  13829  invf  16475  cicsym  16511  cnvtsr  17269  znleval  19951  ordtbas2  21043  ordtcnv  21053  ordtrest2  21056  cnconn  21273  tgqtop  21563  adj1o  28881  fcoinver  29544  fresf1o  29561  fcnvgreu  29600  dfcnv2  29604  cnvordtrestixx  30087  xrge0iifhmeo  30110  mbfmcst  30449  0rrv  30641  elrn3  31778  dfrn6  34213  cnvresrn  34256  dmcoss2  34344  cnvrcl0  38249  conrel2d  38273  relexpaddss  38327  rntrclfvRP  38340  ntrneifv2  38695