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

Definition df-ima 4522
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 4521) and range (df-rn 4520). For an alternate definition, see dfima2 4853. (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 4512 . 2  class  ( A
" B )
41, 2cres 4511 . . 3  class  ( A  |`  B )
54crn 4510 . 2  class  ran  ( A  |`  B )
63, 5wceq 1316 1  wff  ( A
" B )  =  ran  ( A  |`  B )
Colors of variables: wff set class
This definition is referenced by:  resima  4822  resima2  4823  imaeq1  4846  imaeq2  4847  dfima2  4853  nfima  4859  rnresi  4866  resiima  4867  ima0  4868  imadisj  4871  imass1  4884  imass2  4885  ndmima  4886  imaundi  4921  imaundir  4922  inimass  4925  rninxp  4952  imainrect  4954  xpima1  4955  xpima2m  4956  dfrn4  4969  imacnvcnv  4973  imadmres  5001  mptpreima  5002  rnco2  5016  funcnvres  5166  funimacnv  5169  funimaexg  5177  fnima  5211  fores  5324  f1ores  5350  f1orescnv  5351  foimacnv  5353  resdif  5357  funfvima  5617  resfunexgALT  5976  smores2  6159  sbthlemi4  6816  sbthlemi6  6818  sbthlemi8  6820  djuin  6917  djuun  6920  casedm  6939  eninl  6950  eninr  6951  djudm  6958  tgrest  12249  cnconst2  12313  hmeores  12395
  Copyright terms: Public domain W3C validator