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

Definition df-ima 4718
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 20845). Contrast with restriction (df-res 4717) and range (df-rn 4716). For an alternate definition, see dfima2 5030. (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 4708 . 2  class  ( A
" B )
41, 2cres 4707 . . 3  class  ( A  |`  B )
54crn 4706 . 2  class  ran  ( A  |`  B )
63, 5wceq 1632 1  wff  ( A
" B )  =  ran  ( A  |`  B )
Colors of variables: wff set class
This definition is referenced by:  resima  5003  resima2  5004  imaeq1  5023  imaeq2  5024  dfima2  5030  nfima  5036  csbima12gALT  5039  rnresi  5044  resiima  5045  ima0  5046  imadisj  5048  imass1  5064  imass2  5065  ndmima  5066  imaundi  5109  imaundir  5110  rninxp  5133  imainrect  5135  dfrn4  5150  imacnvcnv  5153  imadmres  5181  mptpreima  5182  rnco2  5196  funcnvres  5337  funimacnv  5340  fnima  5378  fores  5476  f1ores  5503  f1orescnv  5504  foimacnv  5506  resdif  5510  resfunexgALT  5754  funfvima  5769  funiunfv  5790  soisores  5840  curry1  6226  curry2  6229  fparlem3  6236  fparlem4  6237  smores2  6387  tz7.44-3  6437  tz7.49c  6474  seqomlem2  6479  seqomlem3  6480  seqomlem4  6481  sbthlem4  6990  sbthlem6  6992  sbthlem8  6994  fodomfi  7151  dffi3  7200  marypha1lem  7202  marypha2lem4  7207  dfsup3OLD  7213  ordtypelem3  7251  ordtypelem9  7257  wdomima2g  7316  rankwflemb  7481  dfac8alem  7672  dfac12lem1  7785  zorn2lem1  8139  ttukeylem3  8154  imadomg  8175  iunfo  8177  fpwwe2lem6  8273  fpwwe2lem9  8276  fpwwe2lem13  8280  gruima  8440  peano5nni  9765  1nn  9773  peano2nn  9774  seqval  11073  hashf1lem1  11409  frmdss2  14501  ghmima  14719  conjsubg  14730  gsumzaddlem  15219  gsumxp  15243  dprd2da  15293  dmdprdsplit2lem  15296  ablfac1b  15321  mplsubrglem  16199  pjdm  16623  tgrest  16906  cnconst2  17027  imacmp  17140  cmpfi  17151  conima  17167  kgencn3  17269  ptpjopn  17322  xkoccn  17329  txkgen  17362  qtoprest  17424  hmeores  17478  txflf  17717  subgntr  17805  opnsubg  17806  clsnsg  17808  tgpconcomp  17811  snclseqg  17814  tsmsf1o  17843  tsmsxplem1  17851  ovolicc2lem4  18895  mbflimsup  19037  itg1addlem4  19070  ellimc2  19243  c1lip3  19362  lhop  19379  dvcnvrelem1  19380  mdegfval  19464  aalioulem3  19730  taylthlem2  19769  efifo  19925  dfrelog  19939  efopnlem2  20020  xrlimcnp  20279  fsumdvdsmul  20451  dchrghm  20511  ex-ima  20845  subgornss  20989  efghgrp  21056  xpima  23217  mbfmcst  23579  0rrv  23669  cvmliftmolem1  23827  cvmlift2lem9a  23849  cvmlift2lem9  23857  rdgprc  24222  dfrdg2  24223  dfon4  24504  domrancur1b  25303  domrancur1c  25305  prsubrtr  25502  ivthALT  26361  cnres2  26586  imaiinfv  26862  diophrw  26941  dnnumch1  27244  fnwe2lem2  27251  lindsmm  27401  hbtlem6  27436  funcoressn  28095  csbima12gALTVD  28989  diaintclN  31870  dibintclN  31979  dihintcl  32156
  Copyright terms: Public domain W3C validator