Definition df-rn 4736

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 4735). For alternate definitions, see dfrn2 4918, dfrn3 4919, and dfrn4 5197. 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 4726	. 2 class ran 𝐴
3	1	ccnv 4724	. . 3 class ◡𝐴
4	3	cdm 4725	. 2 class dom ◡𝐴
5	2, 4	wceq 1397	1 wff ran 𝐴 = dom ◡𝐴

This definition is referenced by:  dfrn2  4918  dmcnvcnv  4956  rncnvcnv  4957  rneq  4959  rnss  4962  brelrng  4963  nfrn  4977  rncoss  5003  rncoeq  5006  cnvimarndm  5100  rnun  5145  rnin  5146  rnxpm  5166  rnxpss  5168  imainrect  5182  rnsnopg  5215  cnvssrndm  5258  cocnvss  5262  unidmrn  5269  dfdm2  5271  cnvexg  5274  fncnv  5396  funcnvres  5403  funimacnv  5406  fimacnvdisj  5521  dff1o4  5591  foimacnv  5601  funcocnv2  5608  f1ompt  5798  errn  6723  funrnfi  7140  sbthlemi5  7159  sbthlemi8  7162  sbthlemi9  7163  casefun  7283  caseinj  7287  djufun  7302  djuinj  7304  ctssdccl  7309  exmidfodomrlemim  7411  znleval  14666