Definition df-rn 4615

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 4614). For alternate definitions, see dfrn2 4792, dfrn3 4793, and dfrn4 5064. 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 4605	. 2 class ran 𝐴
3	1	ccnv 4603	. . 3 class ◡𝐴
4	3	cdm 4604	. 2 class dom ◡𝐴
5	2, 4	wceq 1343	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  4792  dmcnvcnv  4828  rncnvcnv  4829  rneq  4831  rnss  4834  brelrng  4835  nfrn  4849  rncoss  4874  rncoeq  4877  cnvimarndm  4968  rnun  5012  rnin  5013  rnxpm  5033  rnxpss  5035  imainrect  5049  rnsnopg  5082  cnvssrndm  5125  cocnvss  5129  unidmrn  5136  dfdm2  5138  cnvexg  5141  fncnv  5254  funcnvres  5261  funimacnv  5264  fimacnvdisj  5372  dff1o4  5440  foimacnv  5450  funcocnv2  5457  f1ompt  5636  errn  6523  funrnfi  6907  sbthlemi5  6926  sbthlemi8  6929  sbthlemi9  6930  casefun  7050  caseinj  7054  djufun  7069  djuinj  7071  ctssdccl  7076  exmidfodomrlemim  7157