Definition df-rn 4729

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 4728). For alternate definitions, see dfrn2 4909, dfrn3 4910, and dfrn4 5188. 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 4719	. 2 class ran 𝐴
3	1	ccnv 4717	. . 3 class ◡𝐴
4	3	cdm 4718	. 2 class dom ◡𝐴
5	2, 4	wceq 1395	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  4909  dmcnvcnv  4947  rncnvcnv  4948  rneq  4950  rnss  4953  brelrng  4954  nfrn  4968  rncoss  4994  rncoeq  4997  cnvimarndm  5091  rnun  5136  rnin  5137  rnxpm  5157  rnxpss  5159  imainrect  5173  rnsnopg  5206  cnvssrndm  5249  cocnvss  5253  unidmrn  5260  dfdm2  5262  cnvexg  5265  fncnv  5386  funcnvres  5393  funimacnv  5396  fimacnvdisj  5509  dff1o4  5579  foimacnv  5589  funcocnv2  5596  f1ompt  5785  errn  6700  funrnfi  7105  sbthlemi5  7124  sbthlemi8  7127  sbthlemi9  7128  casefun  7248  caseinj  7252  djufun  7267  djuinj  7269  ctssdccl  7274  exmidfodomrlemim  7375  znleval  14611