Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-rn | Unicode 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 4519). For alternate definitions, see dfrn2 4697, dfrn3 4698, and dfrn4 4969. The notation " " is used by Enderton; other authors sometimes use script R or script W. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-rn |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | 1 | crn 4510 | . 2 |
3 | 1 | ccnv 4508 | . . 3 |
4 | 3 | cdm 4509 | . 2 |
5 | 2, 4 | wceq 1316 | 1 |
Colors of variables: wff set class |
This definition is referenced by: dfrn2 4697 dmcnvcnv 4733 rncnvcnv 4734 rneq 4736 rnss 4739 brelrng 4740 nfrn 4754 rncoss 4779 rncoeq 4782 cnvimarndm 4873 rnun 4917 rnin 4918 rnxpm 4938 rnxpss 4940 imainrect 4954 rnsnopg 4987 cnvssrndm 5030 cocnvss 5034 unidmrn 5041 dfdm2 5043 cnvexg 5046 fncnv 5159 funcnvres 5166 funimacnv 5169 fimacnvdisj 5277 dff1o4 5343 foimacnv 5353 funcocnv2 5360 f1ompt 5539 errn 6419 funrnfi 6798 sbthlemi5 6817 sbthlemi8 6820 sbthlemi9 6821 casefun 6938 caseinj 6942 djufun 6957 djuinj 6959 ctssdccl 6964 exmidfodomrlemim 7025 |
Copyright terms: Public domain | W3C validator |