MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ima Unicode version

Definition df-ima 4882
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 } (ex-ima 21738). Contrast with restriction (df-res 4881) and range (df-rn 4880). For an alternate definition, see dfima2 5196. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
df-ima  |-  ( A
" B )  =  ran  ( A  |`  B )

Detailed syntax breakdown of Definition df-ima
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2cima 4872 . 2  class  ( A
" B )
41, 2cres 4871 . . 3  class  ( A  |`  B )
54crn 4870 . 2  class  ran  ( A  |`  B )
63, 5wceq 1652 1  wff  ( A
" B )  =  ran  ( A  |`  B )
Colors of variables: wff set class
This definition is referenced by:  resima  5169  resima2  5170  imaeq1  5189  imaeq2  5190  dfima2  5196  nfima  5202  csbima12gALT  5205  rnresi  5210  resiima  5211  ima0  5212  imadisj  5214  imass1  5230  imass2  5231  ndmima  5232  imaundi  5275  imaundir  5276  inimass  5279  rninxp  5301  imainrect  5303  xpima  5304  dfrn4  5322  imacnvcnv  5325  imadmres  5353  mptpreima  5354  rnco2  5368  funcnvres  5513  funimacnv  5516  fnima  5554  fores  5653  f1ores  5680  f1orescnv  5681  foimacnv  5683  resdif  5687  resfunexgALT  5949  funfvima  5964  funiunfv  5986  soisores  6038  curry1  6429  curry2  6432  fparlem3  6439  fparlem4  6440  smores2  6607  tz7.44-3  6657  tz7.49c  6694  seqomlem2  6699  seqomlem3  6700  seqomlem4  6701  sbthlem4  7211  sbthlem6  7213  sbthlem8  7215  fodomfi  7376  dffi3  7427  marypha1lem  7429  marypha2lem4  7434  dfsup3OLD  7440  ordtypelem3  7478  ordtypelem9  7484  wdomima2g  7543  rankwflemb  7708  dfac8alem  7899  dfac12lem1  8012  zorn2lem1  8365  ttukeylem3  8380  imadomg  8401  iunfo  8403  fpwwe2lem6  8499  fpwwe2lem9  8502  fpwwe2lem13  8506  gruima  8666  peano5nni  9992  1nn  10000  peano2nn  10001  seqval  11322  hashf1lem1  11692  frmdss2  14796  ghmima  15014  conjsubg  15025  gsumzaddlem  15514  gsumxp  15538  dprd2da  15588  dmdprdsplit2lem  15591  ablfac1b  15616  mplsubrglem  16490  pjdm  16922  tgrest  17211  cnconst2  17335  imacmp  17448  cmpfi  17459  conima  17476  kgencn3  17578  ptpjopn  17632  xkoccn  17639  txkgen  17672  qtoprest  17737  hmeores  17791  txflf  18026  subgntr  18124  opnsubg  18125  clsnsg  18127  tgpconcomp  18130  snclseqg  18133  tsmsf1o  18162  tsmsxplem1  18170  fmucndlem  18309  ovolicc2lem4  19404  mbflimsup  19546  itg1addlem4  19579  ellimc2  19752  c1lip3  19871  lhop  19888  dvcnvrelem1  19889  mdegfval  19973  aalioulem3  20239  taylthlem2  20278  efifo  20437  dfrelog  20451  efopnlem2  20536  xrlimcnp  20795  fsumdvdsmul  20968  dchrghm  21028  usgrares1  21412  cusgrares  21469  ex-ima  21738  subgornss  21882  efghgrp  21949  imadifxp  24026  mbfmcst  24597  0rrv  24697  cvmliftmolem1  24956  cvmlift2lem9a  24978  cvmlift2lem9  24986  rdgprc  25406  dfrdg2  25407  dfon4  25688  ivthALT  26275  cnres2  26409  imaiinfv  26677  diophrw  26754  dnnumch1  27056  fnwe2lem2  27063  lindsmm  27213  hbtlem6  27248  funcoressn  27905  hashimarn  28067  csbima12gALTVD  28863  diaintclN  31695  dibintclN  31804  dihintcl  31981
  Copyright terms: Public domain W3C validator