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

Definition df-ima 4276
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 4275) and range (df-rn 4274). For an alternate definition, see dfima2 4588. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
df-ima (AB) = ran (AB)

Detailed syntax breakdown of Definition df-ima
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
31, 2cima 4266 . 2 class (AB)
41, 2cres 4265 . . 3 class (AB)
54crn 4264 . 2 class ran (AB)
63, 5wceq 1226 1 wff (AB) = ran (AB)
Colors of variables: wff set class
This definition is referenced by:  resima  4561  resima2  4562  imaeq1  4581  imaeq2  4582  dfima2  4588  nfima  4594  rnresi  4600  resiima  4601  ima0  4602  imadisj  4605  imass1  4618  imass2  4619  ndmima  4620  imaundi  4654  imaundir  4655  inimass  4658  rninxp  4682  imainrect  4684  xpima1  4685  xpima2m  4686  dfrn4  4699  imacnvcnv  4703  imadmres  4731  mptpreima  4732  rnco2  4746  funcnvres  4889  funimacnv  4892  funimaexg  4900  fnima  4934  fores  5031  f1ores  5057  f1orescnv  5058  foimacnv  5060  resdif  5064  funfvima  5306  resfunexgALT  5651  smores2  5822
  Copyright terms: Public domain W3C validator