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

Definition df-ima 4336
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 4335) and range (df-rn 4334). For an alternate definition, see dfima2 4648. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
df-ima (𝐴𝐵) = ran (𝐴𝐵)

Detailed syntax breakdown of Definition df-ima
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2cima 4326 . 2 class (𝐴𝐵)
41, 2cres 4325 . . 3 class (𝐴𝐵)
54crn 4324 . 2 class ran (𝐴𝐵)
63, 5wceq 1243 1 wff (𝐴𝐵) = ran (𝐴𝐵)
Colors of variables: wff set class
This definition is referenced by:  resima  4621  resima2  4622  imaeq1  4641  imaeq2  4642  dfima2  4648  nfima  4654  rnresi  4660  resiima  4661  ima0  4662  imadisj  4665  imass1  4678  imass2  4679  ndmima  4680  imaundi  4714  imaundir  4715  inimass  4718  rninxp  4742  imainrect  4744  xpima1  4745  xpima2m  4746  dfrn4  4759  imacnvcnv  4763  imadmres  4791  mptpreima  4792  rnco2  4806  funcnvres  4950  funimacnv  4953  funimaexg  4961  fnima  4995  fores  5093  f1ores  5119  f1orescnv  5120  foimacnv  5122  resdif  5126  funfvima  5368  resfunexgALT  5715  smores2  5887
  Copyright terms: Public domain W3C validator