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 class A
1 cB class B
2 0 1 cima class A B
3 0 1 cres class A B
4 3 crn class ran A B
5 2 4 wceq wff A B = ran A B