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

Definition df-rn 4279
 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 4278). For alternate definitions, see dfrn2 4446, dfrn3 4447, and dfrn4 4704. 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 4269 . 2 class ran A
31ccnv 4267 . . 3 class A
43cdm 4268 . 2 class dom A
52, 4wceq 1226 1 wff ran A = dom A
 Colors of variables: wff set class This definition is referenced by:  dfrn2  4446  dmcnvcnv  4481  rncnvcnv  4482  rneq  4484  rnss  4487  brelrng  4488  nfrn  4502  rncoss  4525  rncoeq  4528  cnvimarndm  4612  rnun  4655  rnin  4656  rnxpm  4675  rnxpss  4677  imainrect  4689  rnsnopg  4722  cnvssrndm  4765  unidmrn  4773  dfdm2  4775  cnvexg  4778  fncnv  4887  funcnvres  4894  funimacnv  4897  fimacnvdisj  4995  dff1o4  5055  foimacnv  5065  funcocnv2  5072  f1ompt  5241  errn  6035
 Copyright terms: Public domain W3C validator