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

Definition df-ima 5021
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 25289). Contrast with restriction (df-res 5020) and range (df-rn 5019). For an alternate definition, see dfima2 5349. (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 5011 . 2  class  ( A
" B )
41, 2cres 5010 . . 3  class  ( A  |`  B )
54crn 5009 . 2  class  ran  ( A  |`  B )
63, 5wceq 1395 1  wff  ( A
" B )  =  ran  ( A  |`  B )
Colors of variables: wff setvar class
This definition is referenced by:  resima  5316  resima2  5317  imaeq1  5342  imaeq2  5343  dfima2  5349  nfima  5355  rnresi  5360  resiima  5361  ima0  5362  imadisj  5366  imass1  5381  imass2  5382  ndmima  5383  imaundi  5425  imaundir  5426  inimass  5429  rninxp  5453  imainrect  5455  xpima  5456  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  6148  funiunfv  6161  soisores  6224  resfunexgALT  6762  curry1  6891  curry2  6894  fparlem3  6901  fparlem4  6902  smores2  7043  tz7.44-3  7092  tz7.49c  7129  seqomlem2  7134  seqomlem3  7135  seqomlem4  7136  sbthlem4  7649  sbthlem6  7651  sbthlem8  7653  fodomfi  7817  dffi3  7909  marypha1lem  7911  marypha2lem4  7916  ordtypelem3  7963  ordtypelem9  7969  wdomima2g  8030  rankwflemb  8228  dfac8alem  8427  dfac12lem1  8540  zorn2lem1  8893  ttukeylem3  8908  imadomg  8929  iunfo  8931  fpwwe2lem6  9030  fpwwe2lem9  9033  fpwwe2lem13  9037  gruima  9197  peano5nni  10559  1nn  10567  peano2nn  10568  seqval  12120  hashimarn  12499  hashf1lem1  12507  frmdss2  16157  ghmima  16413  conjsubg  16424  gsumzaddlem  17060  gsumzaddlemOLD  17062  gsumxp  17130  gsumxpOLD  17132  dprd2da  17217  dmdprdsplit2lem  17220  ablfac1b  17247  mplsubrglem  18226  mplsubrglemOLD  18227  pjdm  18864  lindsmm  18989  tgrest  19786  cnconst2  19910  imacmp  20023  cmpfi  20034  conima  20051  kgencn3  20184  ptpjopn  20238  xkoccn  20245  txkgen  20278  qtoprest  20343  hmeores  20397  txflf  20632  subgntr  20730  opnsubg  20731  clsnsg  20733  tgpconcomp  20736  snclseqg  20739  tsmsf1o  20772  tsmsxplem1  20780  fmucndlem  20919  ovolicc2lem4  22056  mbflimsup  22198  itg1addlem4  22231  ellimc2  22406  c1lip3  22525  lhop  22542  dvcnvrelem1  22543  mdegfval  22585  aalioulem3  22855  taylthlem2  22894  efifo  23059  dfrelog  23078  efopnlem2  23163  xrlimcnp  23423  fsumdvdsmul  23596  dchrghm  23656  usgrares1  24536  cusgrares  24598  ex-ima  25289  subgornss  25434  efghgrpOLD  25501  imadifxp  27595  imafi2  27677  ffsrn  27702  mbfmcst  28391  0rrv  28565  cvmliftmolem1  28901  cvmlift2lem9a  28923  cvmlift2lem9  28931  mrsubff1o  29050  msubff1o  29092  rdgprc  29401  dfrdg2  29402  dfon4  29705  ivthALT  30315  cnres2  30421  imaiinfv  30787  diophrw  30854  dnnumch1  31152  fnwe2lem2  31159  hbtlem6  31240  funcoressn  32373  csbima12gALTOLD  33723  csbima12gALTVD  33798  diaintclN  36886  dibintclN  36995  dihintcl  37172  rp-imass  37896
  Copyright terms: Public domain W3C validator