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 4521) and range (df-rn 4520). For an alternate definition, see dfima2 4853. (Contributed by NM, 2-Aug-1994.) |
Ref | Expression |
---|---|
df-ima |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | 1, 2 | cima 4512 | . 2 |
4 | 1, 2 | cres 4511 | . . 3 |
5 | 4 | crn 4510 | . 2 |
6 | 3, 5 | wceq 1316 | 1 |
Colors of variables: wff set class |
This definition is referenced by: resima 4822 resima2 4823 imaeq1 4846 imaeq2 4847 dfima2 4853 nfima 4859 rnresi 4866 resiima 4867 ima0 4868 imadisj 4871 imass1 4884 imass2 4885 ndmima 4886 imaundi 4921 imaundir 4922 inimass 4925 rninxp 4952 imainrect 4954 xpima1 4955 xpima2m 4956 dfrn4 4969 imacnvcnv 4973 imadmres 5001 mptpreima 5002 rnco2 5016 funcnvres 5166 funimacnv 5169 funimaexg 5177 fnima 5211 fores 5324 f1ores 5350 f1orescnv 5351 foimacnv 5353 resdif 5357 funfvima 5617 resfunexgALT 5976 smores2 6159 sbthlemi4 6816 sbthlemi6 6818 sbthlemi8 6820 djuin 6917 djuun 6920 casedm 6939 eninl 6950 eninr 6951 djudm 6958 tgrest 12249 cnconst2 12313 hmeores 12395 |
Copyright terms: Public domain | W3C validator |