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

Definition df-ima 4891
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 21750). Contrast with restriction (df-res 4890) and range (df-rn 4889). For an alternate definition, see dfima2 5205. (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 4881 . 2  class  ( A
" B )
41, 2cres 4880 . . 3  class  ( A  |`  B )
54crn 4879 . 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  5178  resima2  5179  imaeq1  5198  imaeq2  5199  dfima2  5205  nfima  5211  csbima12gALT  5214  rnresi  5219  resiima  5220  ima0  5221  imadisj  5223  imass1  5239  imass2  5240  ndmima  5241  imaundi  5284  imaundir  5285  inimass  5288  rninxp  5310  imainrect  5312  xpima  5313  dfrn4  5331  imacnvcnv  5334  imadmres  5362  mptpreima  5363  rnco2  5377  funcnvres  5522  funimacnv  5525  fnima  5563  fores  5662  f1ores  5689  f1orescnv  5690  foimacnv  5692  resdif  5696  resfunexgALT  5958  funfvima  5973  funiunfv  5995  soisores  6047  curry1  6438  curry2  6441  fparlem3  6448  fparlem4  6449  smores2  6616  tz7.44-3  6666  tz7.49c  6703  seqomlem2  6708  seqomlem3  6709  seqomlem4  6710  sbthlem4  7220  sbthlem6  7222  sbthlem8  7224  fodomfi  7385  dffi3  7436  marypha1lem  7438  marypha2lem4  7443  dfsup3OLD  7449  ordtypelem3  7489  ordtypelem9  7495  wdomima2g  7554  rankwflemb  7719  dfac8alem  7910  dfac12lem1  8023  zorn2lem1  8376  ttukeylem3  8391  imadomg  8412  iunfo  8414  fpwwe2lem6  8510  fpwwe2lem9  8513  fpwwe2lem13  8517  gruima  8677  peano5nni  10003  1nn  10011  peano2nn  10012  seqval  11334  hashf1lem1  11704  frmdss2  14808  ghmima  15026  conjsubg  15037  gsumzaddlem  15526  gsumxp  15550  dprd2da  15600  dmdprdsplit2lem  15603  ablfac1b  15628  mplsubrglem  16502  pjdm  16934  tgrest  17223  cnconst2  17347  imacmp  17460  cmpfi  17471  conima  17488  kgencn3  17590  ptpjopn  17644  xkoccn  17651  txkgen  17684  qtoprest  17749  hmeores  17803  txflf  18038  subgntr  18136  opnsubg  18137  clsnsg  18139  tgpconcomp  18142  snclseqg  18145  tsmsf1o  18174  tsmsxplem1  18182  fmucndlem  18321  ovolicc2lem4  19416  mbflimsup  19558  itg1addlem4  19591  ellimc2  19764  c1lip3  19883  lhop  19900  dvcnvrelem1  19901  mdegfval  19985  aalioulem3  20251  taylthlem2  20290  efifo  20449  dfrelog  20463  efopnlem2  20548  xrlimcnp  20807  fsumdvdsmul  20980  dchrghm  21040  usgrares1  21424  cusgrares  21481  ex-ima  21750  subgornss  21894  efghgrp  21961  imadifxp  24038  mbfmcst  24609  0rrv  24709  cvmliftmolem1  24968  cvmlift2lem9a  24990  cvmlift2lem9  24998  rdgprc  25422  dfrdg2  25423  dfon4  25738  ivthALT  26338  cnres2  26472  imaiinfv  26740  diophrw  26817  dnnumch1  27119  fnwe2lem2  27126  lindsmm  27275  hbtlem6  27310  funcoressn  27967  hashimarn  28163  csbima12gALTVD  29009  diaintclN  31856  dibintclN  31965  dihintcl  32142
  Copyright terms: Public domain W3C validator