![]() |
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 4377) and range (df-rn 4376). For an alternate definition, see dfima2 4694. (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 4368 | . 2 class (𝐴 “ 𝐵) |
4 | 1, 2 | cres 4367 | . . 3 class (𝐴 ↾ 𝐵) |
5 | 4 | crn 4366 | . 2 class ran (𝐴 ↾ 𝐵) |
6 | 3, 5 | wceq 1285 | 1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵) |
Colors of variables: wff set class |
This definition is referenced by: resima 4665 resima2 4666 imaeq1 4687 imaeq2 4688 dfima2 4694 nfima 4700 rnresi 4706 resiima 4707 ima0 4708 imadisj 4711 imass1 4724 imass2 4725 ndmima 4726 imaundi 4760 imaundir 4761 inimass 4764 rninxp 4788 imainrect 4790 xpima1 4791 xpima2m 4792 dfrn4 4805 imacnvcnv 4809 imadmres 4837 mptpreima 4838 rnco2 4852 funcnvres 4997 funimacnv 5000 funimaexg 5008 fnima 5042 fores 5140 f1ores 5166 f1orescnv 5167 foimacnv 5169 resdif 5173 funfvima 5416 resfunexgALT 5762 smores2 5937 |
Copyright terms: Public domain | W3C validator |