Definition df-rn 5095

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 27185). Contrast with domain (defined in df-dm 5094). For alternate definitions, see dfrn2 5281, dfrn3 5282, and dfrn4 5564. 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 5085	. 2 class ran 𝐴
3	1	ccnv 5083	. . 3 class ◡𝐴
4	3	cdm 5084	. 2 class dom ◡𝐴
5	2, 4	wceq 1480	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5281  dmcnvcnv  5318  rncnvcnv  5319  rneq  5321  rnss  5324  brelrng  5325  nfrn  5338  rncoss  5356  rncoeq  5359  cnvimarndm  5455  rnun  5510  rnin  5511  rnxp  5533  rnxpss  5535  imainrect  5544  rnsnopg  5583  cnvssrndm  5626  unidmrn  5634  dfdm2  5636  funcnvpr  5918  funcnvtp  5919  funcnvqp  5920  funcnvqpOLD  5921  fncnv  5930  funcnvres  5935  funimacnv  5938  fimacnvdisj  6050  dff1o4  6112  foimacnv  6121  funcocnv2  6128  f1ompt  6348  nvof1o  6501  cnvexg  7074  tz7.48-3  7499  errn  7724  omxpenlem  8021  sbthlem5  8034  sbthlem8  8037  sbthlem9  8038  fodomr  8071  domss2  8079  rnfi  8209  zorn2lem4  9281  rnct  9307  fpwwe2lem13  9424  trclublem  13684  relexpcnv  13725  relexpnnrn  13735  invf  16368  cicsym  16404  cnvtsr  17162  znleval  19843  ordtbas2  20935  ordtcnv  20945  ordtrest2  20948  cnconn  21165  tgqtop  21455  adj1o  28641  fcoinver  29302  fresf1o  29318  fcnvgreu  29356  dfcnv2  29360  cnvordtrestixx  29783  xrge0iifhmeo  29806  mbfmcst  30144  0rrv  30336  elrn3  31414  cnvrcl0  37452  conrel2d  37476  relexpaddss  37530  rntrclfvRP  37543  ntrneifv2  37899