Definition df-rn 4765

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 4764). For alternate definitions, see dfrn2 4948, dfrn3 4949, and dfrn4 5228. 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 4755	. 2 class ran 𝐴
3	1	ccnv 4753	. . 3 class ◡𝐴
4	3	cdm 4754	. 2 class dom ◡𝐴
5	2, 4	wceq 1398	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  4948  dmcnvcnv  4986  rncnvcnv  4987  rneq  4989  rnss  4992  brelrng  4993  nfrn  5007  rncoss  5033  rncoeq  5036  cnvimarndm  5131  rnun  5176  rnin  5177  rnxpm  5197  rnxpss  5199  imainrect  5213  rnsnopg  5246  cnvssrndm  5289  cocnvss  5293  unidmrn  5300  dfdm2  5302  cnvexg  5305  fncnv  5427  funcnvres  5434  funimacnv  5437  fimacnvdisj  5556  dff1o4  5627  foimacnv  5637  funcocnv2  5644  f1ompt  5833  errn  6802  funrnfi  7222  sbthlemi5  7244  sbthlemi8  7247  sbthlemi9  7248  casefun  7389  caseinj  7393  djufun  7408  djuinj  7410  ctssdccl  7415  exmidfodomrlemim  7517  znleval  14927