Definition df-ima 3197

Description: Define the image of a class. Definition 6.6(2) of [TakeutiZaring] p. 24. For an alternate definition, see dfima2 3411.

Assertion

Ref	Expression
df-ima	⊢ (A “ B) = ran ( A ↾ B)

Detailed syntax breakdown of Definition df-ima

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cima 3179	. 2 class (A “ B)
4	1, 2	cres 3178	. . 3 class (A ↾ B)
5	4	crn 3177	. 2 class ran ( A ↾ B)
6	3, 5	wceq 958	1 wff (A “ B) = ran ( A ↾ B)

This definition is referenced by:  resima 3397  imaeq1 3407  imaeq2 3408  dfima2 3411  rnresi 3424  resiima 3425  ima0 3426  imadisj 3428  imass1 3438  imass2 3439  ndmima 3440  imaun 3466  imaun2 3467  dfrn4 3498  imacnvcnv 3501  imadmres 3504  rnco2 3509  funcnvres 3574  funimacnv 3577  resfunexg 3585  fores 3687  f1orescnv 3710  fvres 3740  funfvima 3858  tz7.44-3 3936  tz7.48-2 3963  tz7.49c 3966  2ndconst 4103  curry1 4104  sbthlem4 4456  sbthlem6 4458  sbthlem8 4460  numthlem 4793  zorn2lem1 4798  imadomg 4816  subtop 7643  subgrnss 8115  ghsubgi 8134  efghgrpilem 8714  dfrelog 8751

Copyright terms: Public domain