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

Definition df-ima 4559
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 4558) and range (df-rn 4557). For an alternate definition, see dfima2 4890. (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 4549 . 2  class  ( A
" B )
41, 2cres 4548 . . 3  class  ( A  |`  B )
54crn 4547 . 2  class  ran  ( A  |`  B )
63, 5wceq 1332 1  wff  ( A
" B )  =  ran  ( A  |`  B )
Colors of variables: wff set class
This definition is referenced by:  resima  4859  resima2  4860  imaeq1  4883  imaeq2  4884  dfima2  4890  nfima  4896  rnresi  4903  resiima  4904  ima0  4905  imadisj  4908  imass1  4921  imass2  4922  ndmima  4923  imaundi  4958  imaundir  4959  inimass  4962  rninxp  4989  imainrect  4991  xpima1  4992  xpima2m  4993  dfrn4  5006  imacnvcnv  5010  imadmres  5038  mptpreima  5039  rnco2  5053  funcnvres  5203  funimacnv  5206  funimaexg  5214  fnima  5248  fores  5361  f1ores  5389  f1orescnv  5390  foimacnv  5392  resdif  5396  funfvima  5656  resfunexgALT  6015  smores2  6198  sbthlemi4  6855  sbthlemi6  6857  sbthlemi8  6859  djuin  6956  djuun  6959  casedm  6978  eninl  6989  eninr  6990  djudm  6997  tgrest  12375  cnconst2  12439  hmeores  12521
  Copyright terms: Public domain W3C validator