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

Definition df-rn 4383
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 4382). For alternate definitions, see dfrn2 4550, dfrn3 4551, and dfrn4 4808. 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 4373 . 2  class  ran  A
31ccnv 4371 . . 3  class  `' A
43cdm 4372 . 2  class  dom  `' A
52, 4wceq 1259 1  wff  ran  A  =  dom  `' A
Colors of variables: wff set class
This definition is referenced by:  dfrn2  4550  dmcnvcnv  4585  rncnvcnv  4586  rneq  4588  rnss  4591  brelrng  4592  nfrn  4606  rncoss  4629  rncoeq  4632  cnvimarndm  4716  rnun  4759  rnin  4760  rnxpm  4779  rnxpss  4781  imainrect  4793  rnsnopg  4826  cnvssrndm  4869  unidmrn  4877  dfdm2  4879  cnvexg  4882  fncnv  4992  funcnvres  4999  funimacnv  5002  fimacnvdisj  5101  dff1o4  5161  foimacnv  5171  funcocnv2  5178  f1ompt  5347  errn  6158
  Copyright terms: Public domain W3C validator