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

Definition df-rn 4271
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 4270). For alternate definitions, see dfrn2 4438, dfrn3 4439, and dfrn4 4696. 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 4261 . 2 class ran A
31ccnv 4259 . . 3 class A
43cdm 4260 . 2 class dom A
52, 4wceq 1223 1 wff ran A = dom A
Colors of variables: wff set class
This definition is referenced by:  dfrn2  4438  dmcnvcnv  4473  rncnvcnv  4474  rneq  4476  rnss  4479  brelrng  4480  nfrn  4494  rncoss  4517  rncoeq  4520  cnvimarndm  4604  rnun  4647  rnin  4648  rnxpm  4667  rnxpss  4669  imainrect  4681  rnsnopg  4714  cnvssrndm  4757  unidmrn  4765  dfdm2  4767  cnvexg  4770  fncnv  4879  funcnvres  4886  funimacnv  4889  fimacnvdisj  4987  dff1o4  5047  foimacnv  5057  funcocnv2  5064  f1ompt  5233  errn  6027
  Copyright terms: Public domain W3C validator