Definition df-rn 4622

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 4621). For alternate definitions, see dfrn2 4799, dfrn3 4800, and dfrn4 5071. 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 4612	. 2 class ran 𝐴
3	1	ccnv 4610	. . 3 class ◡𝐴
4	3	cdm 4611	. 2 class dom ◡𝐴
5	2, 4	wceq 1348	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  4799  dmcnvcnv  4835  rncnvcnv  4836  rneq  4838  rnss  4841  brelrng  4842  nfrn  4856  rncoss  4881  rncoeq  4884  cnvimarndm  4975  rnun  5019  rnin  5020  rnxpm  5040  rnxpss  5042  imainrect  5056  rnsnopg  5089  cnvssrndm  5132  cocnvss  5136  unidmrn  5143  dfdm2  5145  cnvexg  5148  fncnv  5264  funcnvres  5271  funimacnv  5274  fimacnvdisj  5382  dff1o4  5450  foimacnv  5460  funcocnv2  5467  f1ompt  5647  errn  6535  funrnfi  6919  sbthlemi5  6938  sbthlemi8  6941  sbthlemi9  6942  casefun  7062  caseinj  7066  djufun  7081  djuinj  7083  ctssdccl  7088  exmidfodomrlemim  7178