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

Definition df-rn 4376
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 4375). For alternate definitions, see dfrn2 4545, dfrn3 4546, and dfrn4 4805. 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 4366 . 2 class ran 𝐴
31ccnv 4364 . . 3 class 𝐴
43cdm 4365 . 2 class dom 𝐴
52, 4wceq 1285 1 wff ran 𝐴 = dom 𝐴
Colors of variables: wff set class
This definition is referenced by:  dfrn2  4545  dmcnvcnv  4580  rncnvcnv  4581  rneq  4583  rnss  4586  brelrng  4587  nfrn  4601  rncoss  4624  rncoeq  4627  cnvimarndm  4713  rnun  4756  rnin  4757  rnxpm  4776  rnxpss  4778  imainrect  4790  rnsnopg  4823  cnvssrndm  4866  unidmrn  4874  dfdm2  4876  cnvexg  4879  fncnv  4990  funcnvres  4997  funimacnv  5000  fimacnvdisj  5099  dff1o4  5159  foimacnv  5169  funcocnv2  5176  f1ompt  5346  errn  6187  funrnfi  6440
  Copyright terms: Public domain W3C validator