ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-ima Unicode version

Definition df-ima 4358
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 } . Contrast with restriction (df-res 4357) and range (df-rn 4356). For an alternate definition, see dfima2 4670. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
df-ima  |-  ( A
" B )  =  ran  ( A  |`  B )

Detailed syntax breakdown of Definition df-ima
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2cima 4348 . 2  class  ( A
" B )
41, 2cres 4347 . . 3  class  ( A  |`  B )
54crn 4346 . 2  class  ran  ( A  |`  B )
63, 5wceq 1243 1  wff  ( A
" B )  =  ran  ( A  |`  B )
Colors of variables: wff set class
This definition is referenced by:  resima  4643  resima2  4644  imaeq1  4663  imaeq2  4664  dfima2  4670  nfima  4676  rnresi  4682  resiima  4683  ima0  4684  imadisj  4687  imass1  4700  imass2  4701  ndmima  4702  imaundi  4736  imaundir  4737  inimass  4740  rninxp  4764  imainrect  4766  xpima1  4767  xpima2m  4768  dfrn4  4781  imacnvcnv  4785  imadmres  4813  mptpreima  4814  rnco2  4828  funcnvres  4972  funimacnv  4975  funimaexg  4983  fnima  5017  fores  5115  f1ores  5141  f1orescnv  5142  foimacnv  5144  resdif  5148  funfvima  5390  resfunexgALT  5737  smores2  5909
  Copyright terms: Public domain W3C validator