Definition df-rn 4488

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 4487). For alternate definitions, see dfrn2 4665, dfrn3 4666, and dfrn4 4935. 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 4478	. 2 class ran 𝐴
3	1	ccnv 4476	. . 3 class ◡𝐴
4	3	cdm 4477	. 2 class dom ◡𝐴
5	2, 4	wceq 1299	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  4665  dmcnvcnv  4701  rncnvcnv  4702  rneq  4704  rnss  4707  brelrng  4708  nfrn  4722  rncoss  4745  rncoeq  4748  cnvimarndm  4839  rnun  4883  rnin  4884  rnxpm  4904  rnxpss  4906  imainrect  4920  rnsnopg  4953  cnvssrndm  4996  cocnvss  5000  unidmrn  5007  dfdm2  5009  cnvexg  5012  fncnv  5125  funcnvres  5132  funimacnv  5135  fimacnvdisj  5243  dff1o4  5309  foimacnv  5319  funcocnv2  5326  f1ompt  5503  errn  6381  funrnfi  6758  sbthlemi5  6777  sbthlemi8  6780  sbthlemi9  6781  casefun  6885  caseinj  6889  djufun  6904  djuinj  6906  ctssdclemr  6911  exmidfodomrlemim  6966