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 
|- ( A " B ) = ran ( A |` B )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 
 |-  A
1 cB 
 |-  B
2 0 1 cima 
 |-  ( A " B )
3 0 1 cres 
 |-  ( A |` B )
4 3 crn 
 |-  ran ( A |` B )
5 2 4 wceq 
 |-  ( A " B ) = ran ( A |` B )