Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-rn | GIF version |
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 4355). For alternate definitions, see dfrn2 4523, dfrn3 4524, and dfrn4 4781. The notation "ran " is used by Enderton; other authors sometimes use script R or script W. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-rn | ⊢ ran 𝐴 = dom ◡𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | crn 4346 | . 2 class ran 𝐴 |
3 | 1 | ccnv 4344 | . . 3 class ◡𝐴 |
4 | 3 | cdm 4345 | . 2 class dom ◡𝐴 |
5 | 2, 4 | wceq 1243 | 1 wff ran 𝐴 = dom ◡𝐴 |
Colors of variables: wff set class |
This definition is referenced by: dfrn2 4523 dmcnvcnv 4558 rncnvcnv 4559 rneq 4561 rnss 4564 brelrng 4565 nfrn 4579 rncoss 4602 rncoeq 4605 cnvimarndm 4689 rnun 4732 rnin 4733 rnxpm 4752 rnxpss 4754 imainrect 4766 rnsnopg 4799 cnvssrndm 4842 unidmrn 4850 dfdm2 4852 cnvexg 4855 fncnv 4965 funcnvres 4972 funimacnv 4975 fimacnvdisj 5074 dff1o4 5134 foimacnv 5144 funcocnv2 5151 f1ompt 5320 errn 6128 |
Copyright terms: Public domain | W3C validator |