Definition df-rn 4742

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 4741). For alternate definitions, see dfrn2 4924, dfrn3 4925, and dfrn4 5204. 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 4732	. 2 class ran 𝐴
3	1	ccnv 4730	. . 3 class ◡𝐴
4	3	cdm 4731	. 2 class dom ◡𝐴
5	2, 4	wceq 1398	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  4924  dmcnvcnv  4962  rncnvcnv  4963  rneq  4965  rnss  4968  brelrng  4969  nfrn  4983  rncoss  5009  rncoeq  5012  cnvimarndm  5107  rnun  5152  rnin  5153  rnxpm  5173  rnxpss  5175  imainrect  5189  rnsnopg  5222  cnvssrndm  5265  cocnvss  5269  unidmrn  5276  dfdm2  5278  cnvexg  5281  fncnv  5403  funcnvres  5410  funimacnv  5413  fimacnvdisj  5529  dff1o4  5600  foimacnv  5610  funcocnv2  5617  f1ompt  5806  errn  6767  funrnfi  7184  sbthlemi5  7203  sbthlemi8  7206  sbthlemi9  7207  casefun  7344  caseinj  7348  djufun  7363  djuinj  7365  ctssdccl  7370  exmidfodomrlemim  7472  znleval  14749