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

Definition df-rn 4424
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 4423). For alternate definitions, see dfrn2 4594, dfrn3 4595, and dfrn4 4859. 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 4414 . 2  class  ran  A
31ccnv 4412 . . 3  class  `' A
43cdm 4413 . 2  class  dom  `' A
52, 4wceq 1287 1  wff  ran  A  =  dom  `' A
Colors of variables: wff set class
This definition is referenced by:  dfrn2  4594  dmcnvcnv  4629  rncnvcnv  4630  rneq  4632  rnss  4635  brelrng  4636  nfrn  4650  rncoss  4673  rncoeq  4676  cnvimarndm  4765  rnun  4808  rnin  4809  rnxpm  4828  rnxpss  4830  imainrect  4844  rnsnopg  4877  cnvssrndm  4920  cocnvss  4924  unidmrn  4931  dfdm2  4933  cnvexg  4936  fncnv  5047  funcnvres  5054  funimacnv  5057  fimacnvdisj  5160  dff1o4  5226  foimacnv  5236  funcocnv2  5243  f1ompt  5415  errn  6268  funrnfi  6604  sbthlemi5  6617  sbthlemi8  6620  sbthlemi9  6621  casefun  6723  caseinj  6727  djufun  6731  djuinj  6733  exmidfodomrlemim  6774
  Copyright terms: Public domain W3C validator