Definition df-rn 4674

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 4673). For alternate definitions, see dfrn2 4854, dfrn3 4855, and dfrn4 5130. 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 4664	. 2 class ran 𝐴
3	1	ccnv 4662	. . 3 class ◡𝐴
4	3	cdm 4663	. 2 class dom ◡𝐴
5	2, 4	wceq 1364	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  4854  dmcnvcnv  4890  rncnvcnv  4891  rneq  4893  rnss  4896  brelrng  4897  nfrn  4911  rncoss  4936  rncoeq  4939  cnvimarndm  5033  rnun  5078  rnin  5079  rnxpm  5099  rnxpss  5101  imainrect  5115  rnsnopg  5148  cnvssrndm  5191  cocnvss  5195  unidmrn  5202  dfdm2  5204  cnvexg  5207  fncnv  5324  funcnvres  5331  funimacnv  5334  fimacnvdisj  5442  dff1o4  5512  foimacnv  5522  funcocnv2  5529  f1ompt  5713  errn  6614  funrnfi  7008  sbthlemi5  7027  sbthlemi8  7030  sbthlemi9  7031  casefun  7151  caseinj  7155  djufun  7170  djuinj  7172  ctssdccl  7177  exmidfodomrlemim  7268  znleval  14209