ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-rn Unicode version

Definition df-rn 4412
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 4411). For alternate definitions, see dfrn2 4582, dfrn3 4583, and dfrn4 4845. 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  A  =  dom  `' A

Detailed syntax breakdown of Definition df-rn
StepHypRef Expression
1 cA . . 3  class  A
21crn 4402 . 2  class  ran  A
31ccnv 4400 . . 3  class  `' A
43cdm 4401 . 2  class  dom  `' A
52, 4wceq 1285 1  wff  ran  A  =  dom  `' A
Colors of variables: wff set class
This definition is referenced by:  dfrn2  4582  dmcnvcnv  4617  rncnvcnv  4618  rneq  4620  rnss  4623  brelrng  4624  nfrn  4638  rncoss  4661  rncoeq  4664  cnvimarndm  4751  rnun  4794  rnin  4795  rnxpm  4814  rnxpss  4816  imainrect  4830  rnsnopg  4863  cnvssrndm  4906  cocnvss  4910  unidmrn  4917  dfdm2  4919  cnvexg  4922  fncnv  5033  funcnvres  5040  funimacnv  5043  fimacnvdisj  5143  dff1o4  5209  foimacnv  5219  funcocnv2  5226  f1ompt  5395  errn  6244  funrnfi  6576  casefun  6683  caseinj  6687  djufun  6691  djuinj  6693  exmidfodomrlemim  6730
  Copyright terms: Public domain W3C validator