![]() |
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 4656) and range (df-rn 4655). For an alternate definition, see dfima2 4990. (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 4647 | . 2 class (𝐴 “ 𝐵) |
4 | 1, 2 | cres 4646 | . . 3 class (𝐴 ↾ 𝐵) |
5 | 4 | crn 4645 | . 2 class ran (𝐴 ↾ 𝐵) |
6 | 3, 5 | wceq 1364 | 1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵) |
Colors of variables: wff set class |
This definition is referenced by: resima 4958 resima2 4959 imaeq1 4983 imaeq2 4984 dfima2 4990 nfima 4996 rnresi 5003 resiima 5004 ima0 5005 imadisj 5008 imass1 5021 imass2 5022 ndmima 5023 imaundi 5059 imaundir 5060 inimass 5063 rninxp 5090 imainrect 5092 xpima1 5093 xpima2m 5094 dfrn4 5107 imacnvcnv 5111 imadmres 5139 mptpreima 5140 rnco2 5154 funcnvres 5308 funimacnv 5311 funimaexg 5319 fnima 5353 fores 5466 f1ores 5495 f1orescnv 5496 foimacnv 5498 resdif 5502 funfvima 5769 resfunexgALT 6134 smores2 6320 sbthlemi4 6990 sbthlemi6 6992 sbthlemi8 6994 djuin 7094 djuun 7097 casedm 7116 eninl 7127 eninr 7128 djudm 7135 ghmima 13221 conjsubg 13233 tgrest 14146 cnconst2 14210 hmeores 14292 |
Copyright terms: Public domain | W3C validator |