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

Definition df-rn 4520
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 4519). For alternate definitions, see dfrn2 4697, dfrn3 4698, and dfrn4 4969. 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 4510 . 2 class ran 𝐴
31ccnv 4508 . . 3 class 𝐴
43cdm 4509 . 2 class dom 𝐴
52, 4wceq 1316 1 wff ran 𝐴 = dom 𝐴
Colors of variables: wff set class
This definition is referenced by:  dfrn2  4697  dmcnvcnv  4733  rncnvcnv  4734  rneq  4736  rnss  4739  brelrng  4740  nfrn  4754  rncoss  4779  rncoeq  4782  cnvimarndm  4873  rnun  4917  rnin  4918  rnxpm  4938  rnxpss  4940  imainrect  4954  rnsnopg  4987  cnvssrndm  5030  cocnvss  5034  unidmrn  5041  dfdm2  5043  cnvexg  5046  fncnv  5159  funcnvres  5166  funimacnv  5169  fimacnvdisj  5277  dff1o4  5343  foimacnv  5353  funcocnv2  5360  f1ompt  5539  errn  6419  funrnfi  6798  sbthlemi5  6817  sbthlemi8  6820  sbthlemi9  6821  casefun  6938  caseinj  6942  djufun  6957  djuinj  6959  ctssdccl  6964  exmidfodomrlemim  7025
  Copyright terms: Public domain W3C validator