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

Definition df-ima 4955
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 25461). Contrast with restriction (df-res 4954) and range (df-rn 4953). For an alternate definition, see dfima2 5280. (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 4945 . 2  class  ( A
" B )
41, 2cres 4944 . . 3  class  ( A  |`  B )
54crn 4943 . 2  class  ran  ( A  |`  B )
63, 5wceq 1405 1  wff  ( A
" B )  =  ran  ( A  |`  B )
Colors of variables: wff setvar class
This definition is referenced by:  resima  5247  resima2  5248  imaeq1  5273  imaeq2  5274  dfima2  5280  nfima  5286  rnresi  5291  resiima  5292  ima0  5293  imadisj  5297  imass1  5312  imass2  5313  ndmimaOLD  5315  imaundi  5357  imaundir  5358  inimass  5361  rninxp  5385  imainrect  5387  xpima  5388  dfrn4  5405  imacnvcnv  5409  imadmres  5436  mptpreima  5437  rnco2  5451  funcnvres  5594  funimacnv  5597  fnima  5636  fores  5743  f1ores  5769  f1orescnv  5770  foimacnv  5772  resdif  5775  fvrnressn  6022  funfvima  6084  funiunfv  6097  soisores  6162  resfunexgALT  6701  curry1  6830  curry2  6833  fparlem3  6840  fparlem4  6841  smores2  6982  tz7.44-3  7031  tz7.49c  7068  seqomlem2  7073  seqomlem3  7074  seqomlem4  7075  sbthlem4  7588  sbthlem6  7590  sbthlem8  7592  fodomfi  7753  dffi3  7845  marypha1lem  7847  marypha2lem4  7852  ordtypelem3  7899  ordtypelem9  7905  wdomima2g  7966  rankwflemb  8163  dfac8alem  8362  dfac12lem1  8475  zorn2lem1  8828  ttukeylem3  8843  imadomg  8864  iunfo  8866  fpwwe2lem6  8963  fpwwe2lem9  8966  fpwwe2lem13  8970  gruima  9130  peano5nni  10499  1nn  10507  peano2nn  10508  seqval  12072  hashimarn  12452  hashf1lem1  12460  frmdss2  16247  ghmima  16503  conjsubg  16514  gsumzaddlem  17150  gsumzaddlemOLD  17152  gsumxp  17217  dprd2da  17303  dmdprdsplit2lem  17306  ablfac1b  17333  mplsubrglem  18312  mplsubrglemOLD  18313  pjdm  18928  lindsmm  19047  tgrest  19845  cnconst2  19969  imacmp  20082  cmpfi  20093  conima  20110  kgencn3  20243  ptpjopn  20297  xkoccn  20304  txkgen  20337  qtoprest  20402  hmeores  20456  txflf  20691  subgntr  20789  opnsubg  20790  clsnsg  20792  tgpconcomp  20795  snclseqg  20798  tsmsf1o  20831  tsmsxplem1  20839  fmucndlem  20978  ovolicc2lem4  22115  mbflimsup  22257  itg1addlem4  22290  ellimc2  22465  c1lip3  22584  lhop  22601  dvcnvrelem1  22602  mdegfval  22644  aalioulem3  22914  taylthlem2  22953  efifo  23118  dfrelog  23137  efopnlem2  23224  xrlimcnp  23516  fsumdvdsmul  23744  dchrghm  23804  usgrares1  24708  cusgrares  24770  ex-ima  25461  subgornss  25602  efghgrpOLD  25669  imadifxp  27774  fresf1o  27794  imafi2  27853  ffsrn  27879  mbfmcst  28587  0rrv  28776  cvmliftmolem1  29459  cvmlift2lem9a  29481  cvmlift2lem9  29489  mrsubff1o  29608  msubff1o  29650  rdgprc  29900  dfrdg2  29901  dfon4  30204  ivthALT  30551  mptsnunlem  31242  dissneqlem  31244  icoreelrnab  31259  icoreunrn  31264  cnres2  31522  diaintclN  34059  dibintclN  34168  dihintcl  34345  imaiinfv  34968  diophrw  35034  dnnumch1  35333  fnwe2lem2  35340  hbtlem6  35423  rp-imass  35732  csbima12gALTOLD  36633  csbima12gALTVD  36709  funcoressn  37562
  Copyright terms: Public domain W3C validator