Definition df-rn 5645

Description: Define the range of a class. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 30533). Contrast with domain (defined in df-dm 5644). For alternate definitions, see dfrn2 5847, dfrn3 5848, and dfrn4 6170. 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 6039. Not to be confused with "codomain" (see df-f 6506), which may be a superset/superclass of the range (see frn 6679). (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 5635	. 2 class ran 𝐴
3	1	ccnv 5633	. . 3 class ◡𝐴
4	3	cdm 5634	. 2 class dom ◡𝐴
5	2, 4	wceq 1542	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  5847  dmcnvcnv  5892  rncnvcnv  5893  rneq  5895  rnss  5898  brelrng  5900  nfrn  5911  rncoss  5936  rncoeq  5941  cnvimarndm  6052  rnun  6113  rnin  6114  rnxp  6138  rnxpss  6140  imainrect  6149  rnsnopg  6189  cnvssrndm  6239  unidmrn  6247  dfdm2  6249  funcnvpr  6564  funcnvtp  6565  funcnvqp  6566  fncnv  6575  funcnvres  6580  funimacnv  6583  fimacnvdisj  6722  dff1o4  6792  foimacnv  6801  funcocnv2  6809  f1ompt  7067  nvof1o  7238  cnvexg  7878  tz7.48-3  8387  errn  8670  omxpenlem  9020  sbthlem5  9033  sbthlem8  9036  sbthlem9  9037  fodomr  9070  domss2  9078  fodomfir  9242  rnfi  9254  zorn2lem4  10423  rnct  10449  fpwwe2lem12  10567  trclublem  14932  relexpcnv  14972  relexpnnrn  14982  invf  17706  cicsym  17742  cnvtsr  18525  znleval  21526  ordtbas2  23152  ordtcnv  23162  ordtrest2  23165  cnconn  23383  tgqtop  23673  adj1o  31988  fcoinver  32697  fresf1o  32727  fcnvgreu  32768  dfcnv2  32771  preiman0  32806  gsumhashmul  33167  cycpmfvlem  33212  cycpmfv1  33213  cycpmfv2  33214  cycpmfv3  33215  cycpmrn  33243  cnvordtrestixx  34097  xrge0iifhmeo  34120  mbfmcst  34443  0rrv  34635  elrn3  35984  dfrn6  38588  cnvresrn  38628  dmxrn  38667  dmcoss2  38824  cnvrcl0  44010  conrel2d  44049  relexpaddss  44103  rntrclfvRP  44116  ntrneifv2  44465