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 4610) and range (df-rn 4609). For an alternate definition, see dfima2 4942. (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 4601 | . 2 class (𝐴 “ 𝐵) |
4 | 1, 2 | cres 4600 | . . 3 class (𝐴 ↾ 𝐵) |
5 | 4 | crn 4599 | . 2 class ran (𝐴 ↾ 𝐵) |
6 | 3, 5 | wceq 1342 | 1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵) |
Colors of variables: wff set class |
This definition is referenced by: resima 4911 resima2 4912 imaeq1 4935 imaeq2 4936 dfima2 4942 nfima 4948 rnresi 4955 resiima 4956 ima0 4957 imadisj 4960 imass1 4973 imass2 4974 ndmima 4975 imaundi 5010 imaundir 5011 inimass 5014 rninxp 5041 imainrect 5043 xpima1 5044 xpima2m 5045 dfrn4 5058 imacnvcnv 5062 imadmres 5090 mptpreima 5091 rnco2 5105 funcnvres 5255 funimacnv 5258 funimaexg 5266 fnima 5300 fores 5413 f1ores 5441 f1orescnv 5442 foimacnv 5444 resdif 5448 funfvima 5710 resfunexgALT 6070 smores2 6253 sbthlemi4 6916 sbthlemi6 6918 sbthlemi8 6920 djuin 7020 djuun 7023 casedm 7042 eninl 7053 eninr 7054 djudm 7061 tgrest 12716 cnconst2 12780 hmeores 12862 |
Copyright terms: Public domain | W3C validator |