Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-ima | Unicode version |
Description: Define the image of a class (as restricted by another class). Definition 6.6(2) of [TakeutiZaring] p. 24. For example, ( F = { 2 , 6 , 3 , 9 } /\ B = { 1 , 2 } ) -> ( F B ) = { 6 } . Contrast with restriction (df-res 4623) and range (df-rn 4622). For an alternate definition, see dfima2 4955. (Contributed by NM, 2-Aug-1994.) |
Ref | Expression |
---|---|
df-ima |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | 1, 2 | cima 4614 | . 2 |
4 | 1, 2 | cres 4613 | . . 3 |
5 | 4 | crn 4612 | . 2 |
6 | 3, 5 | wceq 1348 | 1 |
Colors of variables: wff set class |
This definition is referenced by: resima 4924 resima2 4925 imaeq1 4948 imaeq2 4949 dfima2 4955 nfima 4961 rnresi 4968 resiima 4969 ima0 4970 imadisj 4973 imass1 4986 imass2 4987 ndmima 4988 imaundi 5023 imaundir 5024 inimass 5027 rninxp 5054 imainrect 5056 xpima1 5057 xpima2m 5058 dfrn4 5071 imacnvcnv 5075 imadmres 5103 mptpreima 5104 rnco2 5118 funcnvres 5271 funimacnv 5274 funimaexg 5282 fnima 5316 fores 5429 f1ores 5457 f1orescnv 5458 foimacnv 5460 resdif 5464 funfvima 5727 resfunexgALT 6087 smores2 6273 sbthlemi4 6937 sbthlemi6 6939 sbthlemi8 6941 djuin 7041 djuun 7044 casedm 7063 eninl 7074 eninr 7075 djudm 7082 tgrest 12963 cnconst2 13027 hmeores 13109 |
Copyright terms: Public domain | W3C validator |