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

Definition df-ima 4601
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 20642). Contrast with restriction (df-res 4600) and range (df-rn 4599). For an alternate definition, see dfima2 4921. (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 4583 . 2  class  ( A
" B )
41, 2cres 4582 . . 3  class  ( A  |`  B )
54crn 4581 . 2  class  ran  (  A  |`  B )
63, 5wceq 1619 1  wff  ( A
" B )  =  ran  (  A  |`  B )
Colors of variables: wff set class
This definition is referenced by:  resima  4894  resima2  4895  imaeq1  4914  imaeq2  4915  dfima2  4921  nfima  4927  csbima12gALT  4930  rnresi  4935  resiima  4936  ima0  4937  imadisj  4939  imass1  4955  imass2  4956  ndmima  4957  imaundi  5000  imaundir  5001  rninxp  5024  imainrect  5026  dfrn4  5040  imacnvcnv  5043  imadmres  5071  mptpreima  5072  rnco2  5086  funcnvres  5178  funimacnv  5181  fnima  5219  fores  5317  f1ores  5344  f1orescnv  5345  foimacnv  5347  resdif  5351  fvres  5394  resfunexgALT  5590  funfvima  5605  funiunfv  5626  soisores  5676  curry1  6062  curry2  6065  fparlem3  6072  fparlem4  6073  smores2  6257  tz7.44-3  6307  tz7.49c  6344  seqomlem2  6349  seqomlem3  6350  seqomlem4  6351  sbthlem4  6859  sbthlem6  6861  sbthlem8  6863  fodomfi  7020  dffi3  7068  marypha1lem  7070  marypha2lem4  7075  dfsup3OLD  7081  ordtypelem3  7119  ordtypelem9  7125  wdomima2g  7184  rankwflemb  7349  dfac8alem  7540  dfac12lem1  7653  zorn2lem1  8007  ttukeylem3  8022  imadomg  8043  iunfo  8045  fpwwe2lem6  8137  fpwwe2lem9  8140  fpwwe2lem13  8144  gruima  8304  peano5nni  9629  1nn  9637  peano2nn  9638  seqval  10935  hashf1lem1  11270  frmdss2  14320  ghmima  14538  conjsubg  14549  gsumzaddlem  15038  gsumxp  15062  dprd2da  15112  dmdprdsplit2lem  15115  ablfac1b  15140  mplsubrglem  16015  pjdm  16439  tgrest  16722  cnconst2  16843  imacmp  16956  cmpfi  16967  conima  16983  kgencn3  17085  ptpjopn  17138  xkoccn  17145  txkgen  17178  qtoprest  17240  hmeores  17294  txflf  17533  subgntr  17621  opnsubg  17622  clsnsg  17624  tgpconcomp  17627  snclseqg  17630  tsmsf1o  17659  tsmsxplem1  17667  ovolicc2lem4  18711  mbflimsup  18853  itg1addlem4  18886  ellimc2  19059  c1lip3  19178  lhop  19195  dvcnvrelem1  19196  mdegfval  19280  aalioulem3  19546  taylthlem2  19585  efifo  19741  dfrelog  19755  efopnlem2  19836  xrlimcnp  20095  fsumdvdsmul  20267  dchrghm  20327  ex-ima  20642  subgornss  20803  efghgrp  20870  cvmliftmolem1  22983  cvmlift2lem9a  23005  cvmlift2lem9  23013  rdgprc  23319  dfrdg2  23320  dfon4  23608  domrancur1b  24366  domrancur1c  24368  prsubrtr  24565  ivthALT  25424  cnres2  25649  imaiinfv  25925  diophrw  26004  dnnumch1  26307  fnwe2lem2  26314  lindsmm  26464  hbtlem6  26499  csbima12gALTVD  27460  diaintclN  30152  dibintclN  30261  dihintcl  30438
  Copyright terms: Public domain W3C validator