![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-ima | GIF 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 4511) and range (df-rn 4510). For an alternate definition, see dfima2 4841. (Contributed by NM, 2-Aug-1994.) |
Ref | Expression |
---|---|
df-ima | ⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | 1, 2 | cima 4502 | . 2 class (𝐴 “ 𝐵) |
4 | 1, 2 | cres 4501 | . . 3 class (𝐴 ↾ 𝐵) |
5 | 4 | crn 4500 | . 2 class ran (𝐴 ↾ 𝐵) |
6 | 3, 5 | wceq 1314 | 1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵) |
Colors of variables: wff set class |
This definition is referenced by: resima 4810 resima2 4811 imaeq1 4834 imaeq2 4835 dfima2 4841 nfima 4847 rnresi 4854 resiima 4855 ima0 4856 imadisj 4859 imass1 4872 imass2 4873 ndmima 4874 imaundi 4909 imaundir 4910 inimass 4913 rninxp 4940 imainrect 4942 xpima1 4943 xpima2m 4944 dfrn4 4957 imacnvcnv 4961 imadmres 4989 mptpreima 4990 rnco2 5004 funcnvres 5154 funimacnv 5157 funimaexg 5165 fnima 5199 fores 5312 f1ores 5338 f1orescnv 5339 foimacnv 5341 resdif 5345 funfvima 5603 resfunexgALT 5962 smores2 6145 sbthlemi4 6800 sbthlemi6 6802 sbthlemi8 6804 djuin 6901 djuun 6904 casedm 6923 eninl 6934 eninr 6935 djudm 6942 tgrest 12181 cnconst2 12244 |
Copyright terms: Public domain | W3C validator |