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

Definition df-rn 4299
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 4298). For alternate definitions, see dfrn2 4466, dfrn3 4467, and dfrn4 4724. 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 4289 . 2 class ran A
31ccnv 4287 . . 3 class A
43cdm 4288 . 2 class dom A
52, 4wceq 1242 1 wff ran A = dom A
Colors of variables: wff set class
This definition is referenced by:  dfrn2  4466  dmcnvcnv  4501  rncnvcnv  4502  rneq  4504  rnss  4507  brelrng  4508  nfrn  4522  rncoss  4545  rncoeq  4548  cnvimarndm  4632  rnun  4675  rnin  4676  rnxpm  4695  rnxpss  4697  imainrect  4709  rnsnopg  4742  cnvssrndm  4785  unidmrn  4793  dfdm2  4795  cnvexg  4798  fncnv  4908  funcnvres  4915  funimacnv  4918  fimacnvdisj  5017  dff1o4  5077  foimacnv  5087  funcocnv2  5094  f1ompt  5263  errn  6064
  Copyright terms: Public domain W3C validator