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

Definition df-ima 4301
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 4300) and range (df-rn 4299). For an alternate definition, see dfima2 4613. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
df-ima 
" 
ran  |`

Detailed syntax breakdown of Definition df-ima
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2cima 4291 . 2 
"
41, 2cres 4290 . . 3  |`
54crn 4289 . 2  ran  |`
63, 5wceq 1242 1  " 
ran  |`
Colors of variables: wff set class
This definition is referenced by:  resima  4586  resima2  4587  imaeq1  4606  imaeq2  4607  dfima2  4613  nfima  4619  rnresi  4625  resiima  4626  ima0  4627  imadisj  4630  imass1  4643  imass2  4644  ndmima  4645  imaundi  4679  imaundir  4680  inimass  4683  rninxp  4707  imainrect  4709  xpima1  4710  xpima2m  4711  dfrn4  4724  imacnvcnv  4728  imadmres  4756  mptpreima  4757  rnco2  4771  funcnvres  4915  funimacnv  4918  funimaexg  4926  fnima  4960  fores  5058  f1ores  5084  f1orescnv  5085  foimacnv  5087  resdif  5091  funfvima  5333  resfunexgALT  5679  smores2  5850
  Copyright terms: Public domain W3C validator