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

Definition df-ima 4657
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 4656) and range (df-rn 4655). For an alternate definition, see dfima2 4990. (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 4647 . 2 class (𝐴𝐵)
41, 2cres 4646 . . 3 class (𝐴𝐵)
54crn 4645 . 2 class ran (𝐴𝐵)
63, 5wceq 1364 1 wff (𝐴𝐵) = ran (𝐴𝐵)
Colors of variables: wff set class
This definition is referenced by:  resima  4958  resima2  4959  imaeq1  4983  imaeq2  4984  dfima2  4990  nfima  4996  rnresi  5003  resiima  5004  ima0  5005  imadisj  5008  imass1  5021  imass2  5022  ndmima  5023  imaundi  5059  imaundir  5060  inimass  5063  rninxp  5090  imainrect  5092  xpima1  5093  xpima2m  5094  dfrn4  5107  imacnvcnv  5111  imadmres  5139  mptpreima  5140  rnco2  5154  funcnvres  5308  funimacnv  5311  funimaexg  5319  fnima  5353  fores  5466  f1ores  5495  f1orescnv  5496  foimacnv  5498  resdif  5502  funfvima  5769  resfunexgALT  6134  smores2  6320  sbthlemi4  6990  sbthlemi6  6992  sbthlemi8  6994  djuin  7094  djuun  7097  casedm  7116  eninl  7127  eninr  7128  djudm  7135  ghmima  13221  conjsubg  13233  tgrest  14146  cnconst2  14210  hmeores  14292
  Copyright terms: Public domain W3C validator