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

Definition df-rn 4518
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 4517). For alternate definitions, see dfrn2 4695, dfrn3 4696, and dfrn4 4967. 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 4508 . 2  class  ran  A
31ccnv 4506 . . 3  class  `' A
43cdm 4507 . 2  class  dom  `' A
52, 4wceq 1314 1  wff  ran  A  =  dom  `' A
Colors of variables: wff set class
This definition is referenced by:  dfrn2  4695  dmcnvcnv  4731  rncnvcnv  4732  rneq  4734  rnss  4737  brelrng  4738  nfrn  4752  rncoss  4777  rncoeq  4780  cnvimarndm  4871  rnun  4915  rnin  4916  rnxpm  4936  rnxpss  4938  imainrect  4952  rnsnopg  4985  cnvssrndm  5028  cocnvss  5032  unidmrn  5039  dfdm2  5041  cnvexg  5044  fncnv  5157  funcnvres  5164  funimacnv  5167  fimacnvdisj  5275  dff1o4  5341  foimacnv  5351  funcocnv2  5358  f1ompt  5537  errn  6417  funrnfi  6796  sbthlemi5  6815  sbthlemi8  6818  sbthlemi9  6819  casefun  6936  caseinj  6940  djufun  6955  djuinj  6957  ctssdccl  6962  exmidfodomrlemim  7021
  Copyright terms: Public domain W3C validator