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

Definition df-ima 4378
 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 4377) and range (df-rn 4376). For an alternate definition, see dfima2 4694. (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 4368 . 2 class (𝐴𝐵)
41, 2cres 4367 . . 3 class (𝐴𝐵)
54crn 4366 . 2 class ran (𝐴𝐵)
63, 5wceq 1285 1 wff (𝐴𝐵) = ran (𝐴𝐵)
 Colors of variables: wff set class This definition is referenced by:  resima  4665  resima2  4666  imaeq1  4687  imaeq2  4688  dfima2  4694  nfima  4700  rnresi  4706  resiima  4707  ima0  4708  imadisj  4711  imass1  4724  imass2  4725  ndmima  4726  imaundi  4760  imaundir  4761  inimass  4764  rninxp  4788  imainrect  4790  xpima1  4791  xpima2m  4792  dfrn4  4805  imacnvcnv  4809  imadmres  4837  mptpreima  4838  rnco2  4852  funcnvres  4997  funimacnv  5000  funimaexg  5008  fnima  5042  fores  5140  f1ores  5166  f1orescnv  5167  foimacnv  5169  resdif  5173  funfvima  5416  resfunexgALT  5762  smores2  5937
 Copyright terms: Public domain W3C validator