Definition df-rn 4762

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 4761). For alternate definitions, see dfrn2 4945, dfrn3 4946, and dfrn4 5225. 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 4752	. 2 class ran 𝐴
3	1	ccnv 4750	. . 3 class ◡𝐴
4	3	cdm 4751	. 2 class dom ◡𝐴
5	2, 4	wceq 1398	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  4945  dmcnvcnv  4983  rncnvcnv  4984  rneq  4986  rnss  4989  brelrng  4990  nfrn  5004  rncoss  5030  rncoeq  5033  cnvimarndm  5128  rnun  5173  rnin  5174  rnxpm  5194  rnxpss  5196  imainrect  5210  rnsnopg  5243  cnvssrndm  5286  cocnvss  5290  unidmrn  5297  dfdm2  5299  cnvexg  5302  fncnv  5424  funcnvres  5431  funimacnv  5434  fimacnvdisj  5553  dff1o4  5624  foimacnv  5634  funcocnv2  5641  f1ompt  5830  errn  6791  funrnfi  7211  sbthlemi5  7233  sbthlemi8  7236  sbthlemi9  7237  casefun  7378  caseinj  7382  djufun  7397  djuinj  7399  ctssdccl  7404  exmidfodomrlemim  7506  znleval  14818