Definition df-rn 4637

Description: Define the range of a class. For example, F = { ⟨ 2 , 6 ⟩, ⟨ 3 , 9 ⟩ } -> ran F = { 6 , 9 } . Contrast with domain (defined in df-dm 4636). For alternate definitions, see dfrn2 4815, dfrn3 4816, and dfrn4 5089. 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 4627	. 2 class ran 𝐴
3	1	ccnv 4625	. . 3 class ◡𝐴
4	3	cdm 4626	. 2 class dom ◡𝐴
5	2, 4	wceq 1353	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  4815  dmcnvcnv  4851  rncnvcnv  4852  rneq  4854  rnss  4857  brelrng  4858  nfrn  4872  rncoss  4897  rncoeq  4900  cnvimarndm  4992  rnun  5037  rnin  5038  rnxpm  5058  rnxpss  5060  imainrect  5074  rnsnopg  5107  cnvssrndm  5150  cocnvss  5154  unidmrn  5161  dfdm2  5163  cnvexg  5166  fncnv  5282  funcnvres  5289  funimacnv  5292  fimacnvdisj  5400  dff1o4  5469  foimacnv  5479  funcocnv2  5486  f1ompt  5667  errn  6556  funrnfi  6940  sbthlemi5  6959  sbthlemi8  6962  sbthlemi9  6963  casefun  7083  caseinj  7087  djufun  7102  djuinj  7104  ctssdccl  7109  exmidfodomrlemim  7199