![]() |
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 = {
![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
df-ima |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | cB |
. . 3
![]() ![]() | |
3 | 1, 2 | cima 4480 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 2 | cres 4479 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | crn 4478 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | wceq 1299 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: resima 4788 resima2 4789 imaeq1 4812 imaeq2 4813 dfima2 4819 nfima 4825 rnresi 4832 resiima 4833 ima0 4834 imadisj 4837 imass1 4850 imass2 4851 ndmima 4852 imaundi 4887 imaundir 4888 inimass 4891 rninxp 4918 imainrect 4920 xpima1 4921 xpima2m 4922 dfrn4 4935 imacnvcnv 4939 imadmres 4967 mptpreima 4968 rnco2 4982 funcnvres 5132 funimacnv 5135 funimaexg 5143 fnima 5177 fores 5290 f1ores 5316 f1orescnv 5317 foimacnv 5319 resdif 5323 funfvima 5581 resfunexgALT 5939 smores2 6121 sbthlemi4 6776 sbthlemi6 6778 sbthlemi8 6780 djuin 6864 djuun 6867 casedm 6886 eninl 6897 eninr 6898 djudm 6905 tgrest 12120 cnconst2 12183 |
Copyright terms: Public domain | W3C validator |