Definition df-rn 4785

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 4784). For alternate definitions, see dfrn2 4968, dfrn3 4969, and dfrn4 5248. 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 4775	. 2 class ran 𝐴
3	1	ccnv 4773	. . 3 class ◡𝐴
4	3	cdm 4774	. 2 class dom ◡𝐴
5	2, 4	wceq 1402	1 wff ran 𝐴 = dom ◡𝐴

This definition is used by:  dfrn2  4968  dmcnvcnv  5006  rncnvcnv  5007  rneq  5009  rnss  5012  brelrng  5013  nfrn  5027  rncoss  5053  rncoeq  5056  cnvimarndm  5151  rnun  5196  rnin  5197  rnxpm  5217  rnxpss  5219  imainrect  5233  rnsnopg  5266  cnvssrndm  5309  cocnvss  5313  unidmrn  5320  dfdm2  5322  cnvexg  5325  fncnv  5447  funcnvres  5454  funimacnv  5457  fimacnvdisj  5576  dff1o4  5647  foimacnv  5657  funcocnv2  5664  f1ompt  5859  errn  6829  funrnfi  7256  sbthlemi5  7278  sbthlemi8  7281  sbthlemi9  7282  casefun  7425  caseinj  7429  djufun  7444  djuinj  7446  ctssdccl  7451  exmidfodomrlemim  7553  znleval  14988