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

Definition df-ima 4414
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 4413) and range (df-rn 4412). For an alternate definition, see dfima2 4731. (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 4404 . 2  class  ( A
" B )
41, 2cres 4403 . . 3  class  ( A  |`  B )
54crn 4402 . 2  class  ran  ( A  |`  B )
63, 5wceq 1285 1  wff  ( A
" B )  =  ran  ( A  |`  B )
Colors of variables: wff set class
This definition is referenced by:  resima  4702  resima2  4703  imaeq1  4724  imaeq2  4725  dfima2  4731  nfima  4737  rnresi  4744  resiima  4745  ima0  4746  imadisj  4749  imass1  4762  imass2  4763  ndmima  4764  imaundi  4798  imaundir  4799  inimass  4802  rninxp  4828  imainrect  4830  xpima1  4831  xpima2m  4832  dfrn4  4845  imacnvcnv  4849  imadmres  4877  mptpreima  4878  rnco2  4892  funcnvres  5040  funimacnv  5043  funimaexg  5051  fnima  5085  fores  5190  f1ores  5216  f1orescnv  5217  foimacnv  5219  resdif  5223  funfvima  5466  resfunexgALT  5816  smores2  5991  djuun  6667  casedm  6684  djudm  6692
  Copyright terms: Public domain W3C validator