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

Definition df-ima 4385
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 4384) and range (df-rn 4383). For an alternate definition, see dfima2 4697. (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 4375 . 2  class  ( A
" B )
41, 2cres 4374 . . 3  class  ( A  |`  B )
54crn 4373 . 2  class  ran  ( A  |`  B )
63, 5wceq 1259 1  wff  ( A
" B )  =  ran  ( A  |`  B )
Colors of variables: wff set class
This definition is referenced by:  resima  4670  resima2  4671  imaeq1  4690  imaeq2  4691  dfima2  4697  nfima  4703  rnresi  4709  resiima  4710  ima0  4711  imadisj  4714  imass1  4727  imass2  4728  ndmima  4729  imaundi  4763  imaundir  4764  inimass  4767  rninxp  4791  imainrect  4793  xpima1  4794  xpima2m  4795  dfrn4  4808  imacnvcnv  4812  imadmres  4840  mptpreima  4841  rnco2  4855  funcnvres  4999  funimacnv  5002  funimaexg  5010  fnima  5044  fores  5142  f1ores  5168  f1orescnv  5169  foimacnv  5171  resdif  5175  funfvima  5417  resfunexgALT  5764  smores2  5939
  Copyright terms: Public domain W3C validator