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

Definition df-rn 4356
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 4355). For alternate definitions, see dfrn2 4523, dfrn3 4524, and dfrn4 4781. 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
StepHypRef Expression
1 cA . . 3 class 𝐴
21crn 4346 . 2 class ran 𝐴
31ccnv 4344 . . 3 class 𝐴
43cdm 4345 . 2 class dom 𝐴
52, 4wceq 1243 1 wff ran 𝐴 = dom 𝐴
Colors of variables: wff set class
This definition is referenced by:  dfrn2  4523  dmcnvcnv  4558  rncnvcnv  4559  rneq  4561  rnss  4564  brelrng  4565  nfrn  4579  rncoss  4602  rncoeq  4605  cnvimarndm  4689  rnun  4732  rnin  4733  rnxpm  4752  rnxpss  4754  imainrect  4766  rnsnopg  4799  cnvssrndm  4842  unidmrn  4850  dfdm2  4852  cnvexg  4855  fncnv  4965  funcnvres  4972  funimacnv  4975  fimacnvdisj  5074  dff1o4  5134  foimacnv  5144  funcocnv2  5151  f1ompt  5320  errn  6128
  Copyright terms: Public domain W3C validator