![]() |
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 4300) and range (df-rn 4299). For an alternate definition, see dfima2 4613. (Contributed by NM, 2-Aug-1994.) |
Ref | Expression |
---|---|
df-ima | ⊢ (A “ B) = ran (A ↾ B) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class A | |
2 | cB | . . 3 class B | |
3 | 1, 2 | cima 4291 | . 2 class (A “ B) |
4 | 1, 2 | cres 4290 | . . 3 class (A ↾ B) |
5 | 4 | crn 4289 | . 2 class ran (A ↾ B) |
6 | 3, 5 | wceq 1242 | 1 wff (A “ B) = ran (A ↾ B) |
Colors of variables: wff set class |
This definition is referenced by: resima 4586 resima2 4587 imaeq1 4606 imaeq2 4607 dfima2 4613 nfima 4619 rnresi 4625 resiima 4626 ima0 4627 imadisj 4630 imass1 4643 imass2 4644 ndmima 4645 imaundi 4679 imaundir 4680 inimass 4683 rninxp 4707 imainrect 4709 xpima1 4710 xpima2m 4711 dfrn4 4724 imacnvcnv 4728 imadmres 4756 mptpreima 4757 rnco2 4771 funcnvres 4915 funimacnv 4918 funimaexg 4926 fnima 4960 fores 5058 f1ores 5084 f1orescnv 5085 foimacnv 5087 resdif 5091 funfvima 5333 resfunexgALT 5679 smores2 5850 |
Copyright terms: Public domain | W3C validator |