![]() |
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 4647 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 2 | cres 4646 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | crn 4645 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | wceq 1364 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: resima 4958 resima2 4959 imaeq1 4983 imaeq2 4984 dfima2 4990 nfima 4996 rnresi 5003 resiima 5004 ima0 5005 imadisj 5008 imass1 5021 imass2 5022 ndmima 5023 imaundi 5059 imaundir 5060 inimass 5063 rninxp 5090 imainrect 5092 xpima1 5093 xpima2m 5094 dfrn4 5107 imacnvcnv 5111 imadmres 5139 mptpreima 5140 rnco2 5154 funcnvres 5308 funimacnv 5311 funimaexg 5319 fnima 5353 fores 5466 f1ores 5495 f1orescnv 5496 foimacnv 5498 resdif 5502 funfvima 5769 resfunexgALT 6133 smores2 6319 sbthlemi4 6989 sbthlemi6 6991 sbthlemi8 6993 djuin 7093 djuun 7096 casedm 7115 eninl 7126 eninr 7127 djudm 7134 ghmima 13204 conjsubg 13216 tgrest 14129 cnconst2 14193 hmeores 14275 |
Copyright terms: Public domain | W3C validator |