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

Definition df-ima 4701
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 20804). Contrast with restriction (df-res 4700) and range (df-rn 4699). For an alternate definition, see dfima2 5013. (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 4691 . 2  class  ( A
" B )
41, 2cres 4690 . . 3  class  ( A  |`  B )
54crn 4689 . 2  class  ran  (  A  |`  B )
63, 5wceq 1624 1  wff  ( A
" B )  =  ran  (  A  |`  B )
Colors of variables: wff set class
This definition is referenced by:  resima  4986  resima2  4987  imaeq1  5006  imaeq2  5007  dfima2  5013  nfima  5019  csbima12gALT  5022  rnresi  5027  resiima  5028  ima0  5029  imadisj  5031  imass1  5047  imass2  5048  ndmima  5049  imaundi  5092  imaundir  5093  rninxp  5116  imainrect  5118  dfrn4  5132  imacnvcnv  5135  imadmres  5163  mptpreima  5164  rnco2  5178  funcnvres  5286  funimacnv  5289  fnima  5327  fores  5425  f1ores  5452  f1orescnv  5453  foimacnv  5455  resdif  5459  fvres  5502  resfunexgALT  5699  funfvima  5714  funiunfv  5735  soisores  5785  curry1  6171  curry2  6174  fparlem3  6181  fparlem4  6182  smores2  6366  tz7.44-3  6416  tz7.49c  6453  seqomlem2  6458  seqomlem3  6459  seqomlem4  6460  sbthlem4  6969  sbthlem6  6971  sbthlem8  6973  fodomfi  7130  dffi3  7179  marypha1lem  7181  marypha2lem4  7186  dfsup3OLD  7192  ordtypelem3  7230  ordtypelem9  7236  wdomima2g  7295  rankwflemb  7460  dfac8alem  7651  dfac12lem1  7764  zorn2lem1  8118  ttukeylem3  8133  imadomg  8154  iunfo  8156  fpwwe2lem6  8252  fpwwe2lem9  8255  fpwwe2lem13  8259  gruima  8419  peano5nni  9744  1nn  9752  peano2nn  9753  seqval  11051  hashf1lem1  11387  frmdss2  14479  ghmima  14697  conjsubg  14708  gsumzaddlem  15197  gsumxp  15221  dprd2da  15271  dmdprdsplit2lem  15274  ablfac1b  15299  mplsubrglem  16177  pjdm  16601  tgrest  16884  cnconst2  17005  imacmp  17118  cmpfi  17129  conima  17145  kgencn3  17247  ptpjopn  17300  xkoccn  17307  txkgen  17340  qtoprest  17402  hmeores  17456  txflf  17695  subgntr  17783  opnsubg  17784  clsnsg  17786  tgpconcomp  17789  snclseqg  17792  tsmsf1o  17821  tsmsxplem1  17829  ovolicc2lem4  18873  mbflimsup  19015  itg1addlem4  19048  ellimc2  19221  c1lip3  19340  lhop  19357  dvcnvrelem1  19358  mdegfval  19442  aalioulem3  19708  taylthlem2  19747  efifo  19903  dfrelog  19917  efopnlem2  19998  xrlimcnp  20257  fsumdvdsmul  20429  dchrghm  20489  ex-ima  20804  subgornss  20965  efghgrp  21032  cvmliftmolem1  23216  cvmlift2lem9a  23238  cvmlift2lem9  23246  rdgprc  23552  dfrdg2  23553  dfon4  23841  domrancur1b  24599  domrancur1c  24601  prsubrtr  24798  ivthALT  25657  cnres2  25882  imaiinfv  26158  diophrw  26237  dnnumch1  26540  fnwe2lem2  26547  lindsmm  26697  hbtlem6  26732  funcoressn  27363  csbima12gALTVD  27941  diaintclN  30515  dibintclN  30624  dihintcl  30801
  Copyright terms: Public domain W3C validator