Definition df-ima 3187

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

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 3169	. 2 class (A"B)
4	1, 2	cres 3168	. . 3 class (A |` B)
5	4	crn 3167	. 2 class ran ( A |` B)
6	3, 5	wceq 955	1 wff (A"B) = ran ( A |` B)

This definition is referenced by:  resima 3387  imaeq1 3397  imaeq2 3398  dfima2 3401  rnresi 3414  resiima 3415  ima0 3416  imadisj 3418  imass1 3428  imass2 3429  ndmima 3430  imaun 3456  imaun2 3457  dfrn4 3488  imacnvcnv 3491  imadmres 3494  rnco2 3499  funcnvres 3564  funimacnv 3567  resfunexg 3575  fores 3676  f1orescnv 3699  fvres 3729  funfvima 3847  tz7.44-3 3925  tz7.48-2 3952  tz7.49c 3955  2ndconst 4090  curry1 4091  sbthlem4 4439  sbthlem6 4441  sbthlem8 4443  numthlem 4766  zorn2lem1 4771  imadomg 4789  subtop 7606  subgrnss 8083  ghsubgi 8102  efghgrpilem 8669  dfrelog 8711

Copyright terms: Public domain