This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-ima

Description: Define the image of a class (as restricted by another class). Definition 6.6(2) of TakeutiZaring p. 24. For example, ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> ( F " B ) = { 6 } ( ex-ima ). Contrast with restriction ( df-res ) and range ( df-rn ). For an alternate definition, see dfima2 . (Contributed by NM, 2-Aug-1994)

		Ref	Expression
	Assertion	df-ima	⊢ ( 𝐴 “ 𝐵 ) = ran ( 𝐴 ↾ 𝐵 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2	0 1	cima	⊢ ( 𝐴 “ 𝐵 )
3	0 1	cres	⊢ ( 𝐴 ↾ 𝐵 )
4	3	crn	⊢ ran ( 𝐴 ↾ 𝐵 )
5	2 4	wceq	⊢ ( 𝐴 “ 𝐵 ) = ran ( 𝐴 ↾ 𝐵 )