Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-ima | Unicode 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 4621) and range (df-rn 4620). For an alternate definition, see dfima2 4953. (Contributed by NM, 2-Aug-1994.) |
Ref | Expression |
---|---|
df-ima |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | 1, 2 | cima 4612 | . 2 |
4 | 1, 2 | cres 4611 | . . 3 |
5 | 4 | crn 4610 | . 2 |
6 | 3, 5 | wceq 1348 | 1 |
Colors of variables: wff set class |
This definition is referenced by: resima 4922 resima2 4923 imaeq1 4946 imaeq2 4947 dfima2 4953 nfima 4959 rnresi 4966 resiima 4967 ima0 4968 imadisj 4971 imass1 4984 imass2 4985 ndmima 4986 imaundi 5021 imaundir 5022 inimass 5025 rninxp 5052 imainrect 5054 xpima1 5055 xpima2m 5056 dfrn4 5069 imacnvcnv 5073 imadmres 5101 mptpreima 5102 rnco2 5116 funcnvres 5269 funimacnv 5272 funimaexg 5280 fnima 5314 fores 5427 f1ores 5455 f1orescnv 5456 foimacnv 5458 resdif 5462 funfvima 5724 resfunexgALT 6084 smores2 6270 sbthlemi4 6933 sbthlemi6 6935 sbthlemi8 6937 djuin 7037 djuun 7040 casedm 7059 eninl 7070 eninr 7071 djudm 7078 tgrest 12922 cnconst2 12986 hmeores 13068 |
Copyright terms: Public domain | W3C validator |