Definition df-rn 5038

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 26482). Contrast with domain (defined in df-dm 5037). For alternate definitions, see dfrn2 5220, dfrn3 5221, and dfrn4 5498. 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 5028	. 2 class ran 𝐴
3	1	ccnv 5026	. . 3 class ◡𝐴
4	3	cdm 5027	. 2 class dom ◡𝐴
5	2, 4	wceq 1474	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5220  dmcnvcnv  5255  rncnvcnv  5256  rneq  5258  rnss  5261  brelrng  5262  nfrn  5275  rncoss  5293  rncoeq  5296  cnvimarndm  5391  rnun  5445  rnin  5446  rnxp  5468  rnxpss  5470  imainrect  5479  rnsnopg  5517  cnvssrndm  5559  unidmrn  5567  dfdm2  5569  funcnvpr  5849  funcnvtp  5850  funcnvqp  5851  funcnvqpOLD  5852  fncnv  5861  funcnvres  5866  funimacnv  5869  fimacnvdisj  5980  dff1o4  6042  foimacnv  6051  funcocnv2  6058  f1ompt  6274  nvof1o  6413  cnvexg  6982  tz7.48-3  7403  errn  7628  omxpenlem  7923  sbthlem5  7936  sbthlem8  7939  sbthlem9  7940  fodomr  7973  domss2  7981  rnfi  8109  zorn2lem4  9181  fpwwe2lem13  9320  trclublem  13530  relexpcnv  13571  relexpnnrn  13581  invf  16199  cicsym  16235  cnvtsr  16993  znleval  19669  ordtbas2  20752  ordtcnv  20762  ordtrest2  20765  cnconn  20982  tgqtop  21272  adj1o  27930  fcoinver  28591  fresf1o  28608  fcnvgreu  28648  dfcnv2  28652  rnct  28672  cnvordtrestixx  29080  xrge0iifhmeo  29103  mbfmcst  29441  0rrv  29633  elrn3  30699  cnvrcl0  36734  conrel2d  36758  relexpaddss  36812  rntrclfvRP  36825  ntrneifv2  37181