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

Definition df-ima 4850
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 21703). Contrast with restriction (df-res 4849) and range (df-rn 4848). For an alternate definition, see dfima2 5164. (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 4840 . 2  class  ( A
" B )
41, 2cres 4839 . . 3  class  ( A  |`  B )
54crn 4838 . 2  class  ran  ( A  |`  B )
63, 5wceq 1649 1  wff  ( A
" B )  =  ran  ( A  |`  B )
Colors of variables: wff set class
This definition is referenced by:  resima  5137  resima2  5138  imaeq1  5157  imaeq2  5158  dfima2  5164  nfima  5170  csbima12gALT  5173  rnresi  5178  resiima  5179  ima0  5180  imadisj  5182  imass1  5198  imass2  5199  ndmima  5200  imaundi  5243  imaundir  5244  inimass  5247  rninxp  5269  imainrect  5271  xpima  5272  dfrn4  5290  imacnvcnv  5293  imadmres  5321  mptpreima  5322  rnco2  5336  funcnvres  5481  funimacnv  5484  fnima  5522  fores  5621  f1ores  5648  f1orescnv  5649  foimacnv  5651  resdif  5655  resfunexgALT  5917  funfvima  5932  funiunfv  5954  soisores  6006  curry1  6397  curry2  6400  fparlem3  6407  fparlem4  6408  smores2  6575  tz7.44-3  6625  tz7.49c  6662  seqomlem2  6667  seqomlem3  6668  seqomlem4  6669  sbthlem4  7179  sbthlem6  7181  sbthlem8  7183  fodomfi  7344  dffi3  7394  marypha1lem  7396  marypha2lem4  7401  dfsup3OLD  7407  ordtypelem3  7445  ordtypelem9  7451  wdomima2g  7510  rankwflemb  7675  dfac8alem  7866  dfac12lem1  7979  zorn2lem1  8332  ttukeylem3  8347  imadomg  8368  iunfo  8370  fpwwe2lem6  8466  fpwwe2lem9  8469  fpwwe2lem13  8473  gruima  8633  peano5nni  9959  1nn  9967  peano2nn  9968  seqval  11289  hashf1lem1  11659  frmdss2  14763  ghmima  14981  conjsubg  14992  gsumzaddlem  15481  gsumxp  15505  dprd2da  15555  dmdprdsplit2lem  15558  ablfac1b  15583  mplsubrglem  16457  pjdm  16889  tgrest  17177  cnconst2  17301  imacmp  17414  cmpfi  17425  conima  17441  kgencn3  17543  ptpjopn  17597  xkoccn  17604  txkgen  17637  qtoprest  17702  hmeores  17756  txflf  17991  subgntr  18089  opnsubg  18090  clsnsg  18092  tgpconcomp  18095  snclseqg  18098  tsmsf1o  18127  tsmsxplem1  18135  fmucndlem  18274  ovolicc2lem4  19369  mbflimsup  19511  itg1addlem4  19544  ellimc2  19717  c1lip3  19836  lhop  19853  dvcnvrelem1  19854  mdegfval  19938  aalioulem3  20204  taylthlem2  20243  efifo  20402  dfrelog  20416  efopnlem2  20501  xrlimcnp  20760  fsumdvdsmul  20933  dchrghm  20993  usgrares1  21377  cusgrares  21434  ex-ima  21703  subgornss  21847  efghgrp  21914  imadifxp  23991  mbfmcst  24562  0rrv  24662  cvmliftmolem1  24921  cvmlift2lem9a  24943  cvmlift2lem9  24951  rdgprc  25365  dfrdg2  25366  dfon4  25647  ivthALT  26228  cnres2  26362  imaiinfv  26630  diophrw  26707  dnnumch1  27009  fnwe2lem2  27016  lindsmm  27166  hbtlem6  27201  funcoressn  27858  hashimarn  27994  csbima12gALTVD  28718  diaintclN  31541  dibintclN  31650  dihintcl  31827
  Copyright terms: Public domain W3C validator