Definition df-rn 4783

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 4782). For alternate definitions, see dfrn2 4966, dfrn3 4967, and dfrn4 5246. 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 4773	. 2 class ran 𝐴
3	1	ccnv 4771	. . 3 class ◡𝐴
4	3	cdm 4772	. 2 class dom ◡𝐴
5	2, 4	wceq 1402	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  4966  dmcnvcnv  5004  rncnvcnv  5005  rneq  5007  rnss  5010  brelrng  5011  nfrn  5025  rncoss  5051  rncoeq  5054  cnvimarndm  5149  rnun  5194  rnin  5195  rnxpm  5215  rnxpss  5217  imainrect  5231  rnsnopg  5264  cnvssrndm  5307  cocnvss  5311  unidmrn  5318  dfdm2  5320  cnvexg  5323  fncnv  5445  funcnvres  5452  funimacnv  5455  fimacnvdisj  5574  dff1o4  5645  foimacnv  5655  funcocnv2  5662  f1ompt  5853  errn  6822  funrnfi  7249  sbthlemi5  7271  sbthlemi8  7274  sbthlemi9  7275  casefun  7418  caseinj  7422  djufun  7437  djuinj  7439  ctssdccl  7444  exmidfodomrlemim  7546  znleval  14963