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

Definition df-ima 4281
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 4280) and range (df-rn 4279). For an alternate definition, see dfima2 4593. (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 4271 . 2 class (AB)
41, 2cres 4270 . . 3 class (AB)
54crn 4269 . 2 class ran (AB)
63, 5wceq 1226 1 wff (AB) = ran (AB)
Colors of variables: wff set class
This definition is referenced by:  resima  4566  resima2  4567  imaeq1  4586  imaeq2  4587  dfima2  4593  nfima  4599  rnresi  4605  resiima  4606  ima0  4607  imadisj  4610  imass1  4623  imass2  4624  ndmima  4625  imaundi  4659  imaundir  4660  inimass  4663  rninxp  4687  imainrect  4689  xpima1  4690  xpima2m  4691  dfrn4  4704  imacnvcnv  4708  imadmres  4736  mptpreima  4737  rnco2  4751  funcnvres  4894  funimacnv  4897  funimaexg  4905  fnima  4939  fores  5036  f1ores  5062  f1orescnv  5063  foimacnv  5065  resdif  5069  funfvima  5311  resfunexgALT  5656  smores2  5827
  Copyright terms: Public domain W3C validator