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

Definition df-rn 4554
 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 4553). For alternate definitions, see dfrn2 4731, dfrn3 4732, and dfrn4 5003. 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 4544 . 2 class ran 𝐴
31ccnv 4542 . . 3 class 𝐴
43cdm 4543 . 2 class dom 𝐴
52, 4wceq 1332 1 wff ran 𝐴 = dom 𝐴
 Colors of variables: wff set class This definition is referenced by:  dfrn2  4731  dmcnvcnv  4767  rncnvcnv  4768  rneq  4770  rnss  4773  brelrng  4774  nfrn  4788  rncoss  4813  rncoeq  4816  cnvimarndm  4907  rnun  4951  rnin  4952  rnxpm  4972  rnxpss  4974  imainrect  4988  rnsnopg  5021  cnvssrndm  5064  cocnvss  5068  unidmrn  5075  dfdm2  5077  cnvexg  5080  fncnv  5193  funcnvres  5200  funimacnv  5203  fimacnvdisj  5311  dff1o4  5379  foimacnv  5389  funcocnv2  5396  f1ompt  5575  errn  6455  funrnfi  6834  sbthlemi5  6853  sbthlemi8  6856  sbthlemi9  6857  casefun  6974  caseinj  6978  djufun  6993  djuinj  6995  ctssdccl  7000  exmidfodomrlemim  7070
 Copyright terms: Public domain W3C validator