Definition df-ima 3272

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

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 3254	. 2 class (A"B)
4	1, 2	cres 3253	. . 3 class (A |` B)
5	4	crn 3252	. 2 class ran ( A |` B)
6	3, 5	wceq 992	1 wff (A"B) = ran ( A |` B)

This definition is referenced by:  resima 3481  imaeq1 3491  imaeq2 3492  dfima2 3497  rnresi 3510  resiima 3511  ima0 3512  imadisj 3514  imass1 3524  imass2 3525  ndmima 3526  imaundi 3545  imaundir 3546  dfrn4 3590  imacnvcnv 3593  imadmres 3596  rnco2 3606  funcnvres 3673  funimacnv 3676  resfunexg 3685  fores 3789  f1orescnv 3812  foimacnv 3814  resdif 3816  fvres 3845  funfvima 3966  curry1 4193  curry2 4196  tz7.44-3 4231  tz7.48-2 4258  tz7.49c 4261  sbthlem4 4595  sbthlem6 4597  sbthlem8 4599  numthlem 4929  zorn2lem1 4934  imadomg 4952  subtop 7858  subgrnss 8361  ghsubgi 8379  efghgrpilem 8991  dfrelog 9028  imrescl 10807  ordtypelem1 11427  ordtypelem6 11432  ordtypelem7 11433  ivthALT 11515  filnetlem5 11767  filnet 11768  ssga 11777  heiborlem33 12043

Copyright terms: Public domain