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

Definition df-ima 4424
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 4423) and range (df-rn 4422). For an alternate definition, see dfima2 4743. (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 4414 . 2  class  ( A
" B )
41, 2cres 4413 . . 3  class  ( A  |`  B )
54crn 4412 . 2  class  ran  ( A  |`  B )
63, 5wceq 1287 1  wff  ( A
" B )  =  ran  ( A  |`  B )
Colors of variables: wff set class
This definition is referenced by:  resima  4712  resima2  4713  imaeq1  4736  imaeq2  4737  dfima2  4743  nfima  4749  rnresi  4756  resiima  4757  ima0  4758  imadisj  4761  imass1  4774  imass2  4775  ndmima  4776  imaundi  4810  imaundir  4811  inimass  4814  rninxp  4840  imainrect  4842  xpima1  4843  xpima2m  4844  dfrn4  4857  imacnvcnv  4861  imadmres  4889  mptpreima  4890  rnco2  4904  funcnvres  5052  funimacnv  5055  funimaexg  5063  fnima  5097  fores  5205  f1ores  5231  f1orescnv  5232  foimacnv  5234  resdif  5238  funfvima  5487  resfunexgALT  5838  smores2  6013  sbthlemi4  6613  sbthlemi6  6615  sbthlemi8  6617  djuun  6704  casedm  6721  djudm  6729
  Copyright terms: Public domain W3C validator