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

Definition df-ima 4624
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 4623) and range (df-rn 4622). For an alternate definition, see dfima2 4955. (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 4614 . 2  class  ( A
" B )
41, 2cres 4613 . . 3  class  ( A  |`  B )
54crn 4612 . 2  class  ran  ( A  |`  B )
63, 5wceq 1348 1  wff  ( A
" B )  =  ran  ( A  |`  B )
Colors of variables: wff set class
This definition is referenced by:  resima  4924  resima2  4925  imaeq1  4948  imaeq2  4949  dfima2  4955  nfima  4961  rnresi  4968  resiima  4969  ima0  4970  imadisj  4973  imass1  4986  imass2  4987  ndmima  4988  imaundi  5023  imaundir  5024  inimass  5027  rninxp  5054  imainrect  5056  xpima1  5057  xpima2m  5058  dfrn4  5071  imacnvcnv  5075  imadmres  5103  mptpreima  5104  rnco2  5118  funcnvres  5271  funimacnv  5274  funimaexg  5282  fnima  5316  fores  5429  f1ores  5457  f1orescnv  5458  foimacnv  5460  resdif  5464  funfvima  5727  resfunexgALT  6087  smores2  6273  sbthlemi4  6937  sbthlemi6  6939  sbthlemi8  6941  djuin  7041  djuun  7044  casedm  7063  eninl  7074  eninr  7075  djudm  7082  tgrest  12963  cnconst2  13027  hmeores  13109
  Copyright terms: Public domain W3C validator