Definition df-ima 2431

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

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 2413	. 2 class (A"B)
4	1, 2	cres 2412	. . 3 class (A |` B)
5	4	crn 2411	. 2 class ran (A |` B)
6	3, 5	wceq 1091	1 wff (A"B) = ran (A |` B)

This definition is referenced by:  resima 2595  imaeq1 2602  imaeq2 2603  dfima2 2604  rnresi 2614  ima0 2615  imass1 2621  imass2 2622  ndmima 2623  imaun 2647  funcnvres 2710  funimacnv 2711  resfunexg 2717  fores 2794  fvres 2840  funfvima 2904  tz7.44-3 2968  tz7.48-2 2995  tz7.49c 2998  sbthlem4 3352  sbthlem6 3354  sbthlem8 3356  numthlem 3598  zornlem1 3603  imadomg 3616

metamath.org