Definition df-ima 3191

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

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 3173	. 2 class (A"B)
4	1, 2	cres 3172	. . 3 class (A |` B)
5	4	crn 3171	. 2 class ran ( A |` B)
6	3, 5	wceq 956	1 wff (A"B) = ran ( A |` B)

This definition is referenced by:  resima 3391  imaeq1 3401  imaeq2 3402  dfima2 3405  rnresi 3418  resiima 3419  ima0 3420  imadisj 3422  imass1 3432  imass2 3433  ndmima 3434  imaun 3460  imaun2 3461  dfrn4 3492  imacnvcnv 3495  imadmres 3498  rnco2 3503  funcnvres 3568  funimacnv 3571  resfunexg 3579  fores 3681  f1orescnv 3704  fvres 3734  funfvima 3852  tz7.44-3 3930  tz7.48-2 3957  tz7.49c 3960  2ndconst 4097  curry1 4098  sbthlem4 4450  sbthlem6 4452  sbthlem8 4454  numthlem 4783  zorn2lem1 4788  imadomg 4806  subtop 7646  subgrnss 8119  ghsubgi 8138  efghgrpilem 8719  dfrelog 8756

Copyright terms: Public domain