Definition df-rn 5125

Description: Define the range of a class. For example, F = { <. 2 , 6 >. , <. 3 , 9 >. } -> ran F = { 6 , 9 } (ex-rn 27297). Contrast with domain (defined in df-dm 5124). For alternate definitions, see dfrn2 5311, dfrn3 5312, and dfrn4 5595. 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 A = dom `' A

Detailed syntax breakdown of Definition df-rn

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	crn 5115	. 2 class ran A
3	1	ccnv 5113	. . 3 class `' A
4	3	cdm 5114	. 2 class dom `' A
5	2, 4	wceq 1483	1 wff ran A = dom `' A

This definition is referenced by:  dfrn2  5311  dmcnvcnv  5348  rncnvcnv  5349  rneq  5351  rnss  5354  brelrng  5355  nfrn  5368  rncoss  5386  rncoeq  5389  cnvimarndm  5486  rnun  5541  rnin  5542  rnxp  5564  rnxpss  5566  imainrect  5575  rnsnopg  5614  cnvssrndm  5657  unidmrn  5665  dfdm2  5667  funcnvpr  5950  funcnvtp  5951  funcnvqp  5952  funcnvqpOLD  5953  fncnv  5962  funcnvres  5967  funimacnv  5970  fimacnvdisj  6083  dff1o4  6145  foimacnv  6154  funcocnv2  6161  f1ompt  6382  nvof1o  6536  cnvexg  7112  tz7.48-3  7539  errn  7764  omxpenlem  8061  sbthlem5  8074  sbthlem8  8077  sbthlem9  8078  fodomr  8111  domss2  8119  rnfi  8249  zorn2lem4  9321  rnct  9347  fpwwe2lem13  9464  trclublem  13734  relexpcnv  13775  relexpnnrn  13785  invf  16428  cicsym  16464  cnvtsr  17222  znleval  19903  ordtbas2  20995  ordtcnv  21005  ordtrest2  21008  cnconn  21225  tgqtop  21515  adj1o  28753  fcoinver  29418  fresf1o  29433  fcnvgreu  29472  dfcnv2  29476  cnvordtrestixx  29959  xrge0iifhmeo  29982  mbfmcst  30321  0rrv  30513  elrn3  31652  dfrn6  34072  cnvresrn  34116  cnvrcl0  37932  conrel2d  37956  relexpaddss  38010  rntrclfvRP  38023  ntrneifv2  38378