HomeRelated theorems
Unicode version
| Home |
Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Define the image of a class. Definition 6.6(2) of [TakeutiZaring] p. 24. For an alternate definition, see dfima2 3389. |
| Ref | Expression |
|---|---|
| df-ima |
         |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA |
. . 3
 | |
| 2 | cB |
. . 3
| |
| 3 | 1, 2 | cima 3163 |
. 2
|
| 4 | 1, 2 | cres 3162 |
. . 3
|
| 5 | 4 | crn 3161 |
. 2
|
| 6 | 3, 5 | wceq 953 |
1
 |
| Colors of variables: wff set class |
| This definition is referenced by: resima 3375 imaeq1 3385 imaeq2 3386 dfima2 3389 rnresi 3402 resiima 3403 ima0 3404 imadisj 3406 imass1 3416 imass2 3417 ndmima 3418 imaun 3446 imaun2 3447 dfrn4 3478 imacnvcnv 3481 imadmres 3484 rnco2 3489 funcnvres 3554 funimacnv 3557 resfunexg 3565 fores 3666 f1orescnv 3689 fvres 3719 funfvima 3837 tz7.44-3 3915 tz7.48-2 3942 tz7.49c 3945 2ndconst 4081 curry1 4082 sbthlem4 4430 sbthlem6 4432 sbthlem8 4434 numthlem 4755 zorn2lem1 4760 imadomg 4778 subtop 7588 subgrnss 8056 ghsubgi 8075 efghgrpilem 8634 dfrelog 8678 |