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

Definition df-ima 5018
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 24995). Contrast with restriction (df-res 5017) and range (df-rn 5016). For an alternate definition, see dfima2 5345. (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 5008 . 2  class  ( A
" B )
41, 2cres 5007 . . 3  class  ( A  |`  B )
54crn 5006 . 2  class  ran  ( A  |`  B )
63, 5wceq 1379 1  wff  ( A
" B )  =  ran  ( A  |`  B )
Colors of variables: wff setvar class
This definition is referenced by:  resima  5312  resima2  5313  imaeq1  5338  imaeq2  5339  dfima2  5345  nfima  5351  rnresi  5356  resiima  5357  ima0  5358  imadisj  5362  imass1  5377  imass2  5378  ndmima  5379  imaundi  5424  imaundir  5425  inimass  5428  rninxp  5452  imainrect  5454  xpima  5455  dfrn4  5473  imacnvcnv  5478  imadmres  5505  mptpreima  5506  rnco2  5520  funcnvres  5663  funimacnv  5666  fnima  5705  fores  5810  f1ores  5836  f1orescnv  5837  foimacnv  5839  resdif  5842  fvrnressn  6087  funfvima  6146  funiunfv  6159  soisores  6222  resfunexgALT  6758  curry1  6887  curry2  6890  fparlem3  6897  fparlem4  6898  smores2  7037  tz7.44-3  7086  tz7.49c  7123  seqomlem2  7128  seqomlem3  7129  seqomlem4  7130  sbthlem4  7642  sbthlem6  7644  sbthlem8  7646  fodomfi  7811  dffi3  7903  marypha1lem  7905  marypha2lem4  7910  dfsup3OLD  7916  ordtypelem3  7957  ordtypelem9  7963  wdomima2g  8024  rankwflemb  8223  dfac8alem  8422  dfac12lem1  8535  zorn2lem1  8888  ttukeylem3  8903  imadomg  8924  iunfo  8926  fpwwe2lem6  9025  fpwwe2lem9  9028  fpwwe2lem13  9032  gruima  9192  peano5nni  10551  1nn  10559  peano2nn  10560  seqval  12098  hashimarn  12476  hashf1lem1  12484  frmdss2  15902  ghmima  16158  conjsubg  16169  gsumzaddlem  16805  gsumzaddlemOLD  16807  gsumxp  16875  gsumxpOLD  16877  dprd2da  16961  dmdprdsplit2lem  16964  ablfac1b  16991  mplsubrglem  17968  mplsubrglemOLD  17969  pjdm  18605  lindsmm  18730  tgrest  19526  cnconst2  19650  imacmp  19763  cmpfi  19774  conima  19792  kgencn3  19925  ptpjopn  19979  xkoccn  19986  txkgen  20019  qtoprest  20084  hmeores  20138  txflf  20373  subgntr  20471  opnsubg  20472  clsnsg  20474  tgpconcomp  20477  snclseqg  20480  tsmsf1o  20513  tsmsxplem1  20521  fmucndlem  20660  ovolicc2lem4  21797  mbflimsup  21939  itg1addlem4  21972  ellimc2  22147  c1lip3  22266  lhop  22283  dvcnvrelem1  22284  mdegfval  22326  aalioulem3  22595  taylthlem2  22634  efifo  22798  dfrelog  22817  efopnlem2  22902  xrlimcnp  23162  fsumdvdsmul  23335  dchrghm  23395  usgrares1  24242  cusgrares  24304  ex-ima  24995  subgornss  25139  efghgrp  25206  imadifxp  27289  ffsrn  27383  mbfmcst  28062  0rrv  28222  cvmliftmolem1  28558  cvmlift2lem9a  28580  cvmlift2lem9  28588  mrsubff1o  28707  msubff1o  28749  rdgprc  29161  dfrdg2  29162  dfon4  29477  ivthALT  30087  cnres2  30193  imaiinfv  30559  diophrw  30626  dnnumch1  30924  fnwe2lem2  30931  hbtlem6  31012  funcoressn  32008  csbima12gALTOLD  33108  csbima12gALTVD  33183  diaintclN  36261  dibintclN  36370  dihintcl  36547  rp-imass  37205
  Copyright terms: Public domain W3C validator