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

Definition df-ima 4858
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 21711). Contrast with restriction (df-res 4857) and range (df-rn 4856). For an alternate definition, see dfima2 5172. (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 4848 . 2  class  ( A
" B )
41, 2cres 4847 . . 3  class  ( A  |`  B )
54crn 4846 . 2  class  ran  ( A  |`  B )
63, 5wceq 1649 1  wff  ( A
" B )  =  ran  ( A  |`  B )
Colors of variables: wff set class
This definition is referenced by:  resima  5145  resima2  5146  imaeq1  5165  imaeq2  5166  dfima2  5172  nfima  5178  csbima12gALT  5181  rnresi  5186  resiima  5187  ima0  5188  imadisj  5190  imass1  5206  imass2  5207  ndmima  5208  imaundi  5251  imaundir  5252  inimass  5255  rninxp  5277  imainrect  5279  xpima  5280  dfrn4  5298  imacnvcnv  5301  imadmres  5329  mptpreima  5330  rnco2  5344  funcnvres  5489  funimacnv  5492  fnima  5530  fores  5629  f1ores  5656  f1orescnv  5657  foimacnv  5659  resdif  5663  resfunexgALT  5925  funfvima  5940  funiunfv  5962  soisores  6014  curry1  6405  curry2  6408  fparlem3  6415  fparlem4  6416  smores2  6583  tz7.44-3  6633  tz7.49c  6670  seqomlem2  6675  seqomlem3  6676  seqomlem4  6677  sbthlem4  7187  sbthlem6  7189  sbthlem8  7191  fodomfi  7352  dffi3  7402  marypha1lem  7404  marypha2lem4  7409  dfsup3OLD  7415  ordtypelem3  7453  ordtypelem9  7459  wdomima2g  7518  rankwflemb  7683  dfac8alem  7874  dfac12lem1  7987  zorn2lem1  8340  ttukeylem3  8355  imadomg  8376  iunfo  8378  fpwwe2lem6  8474  fpwwe2lem9  8477  fpwwe2lem13  8481  gruima  8641  peano5nni  9967  1nn  9975  peano2nn  9976  seqval  11297  hashf1lem1  11667  frmdss2  14771  ghmima  14989  conjsubg  15000  gsumzaddlem  15489  gsumxp  15513  dprd2da  15563  dmdprdsplit2lem  15566  ablfac1b  15591  mplsubrglem  16465  pjdm  16897  tgrest  17185  cnconst2  17309  imacmp  17422  cmpfi  17433  conima  17449  kgencn3  17551  ptpjopn  17605  xkoccn  17612  txkgen  17645  qtoprest  17710  hmeores  17764  txflf  17999  subgntr  18097  opnsubg  18098  clsnsg  18100  tgpconcomp  18103  snclseqg  18106  tsmsf1o  18135  tsmsxplem1  18143  fmucndlem  18282  ovolicc2lem4  19377  mbflimsup  19519  itg1addlem4  19552  ellimc2  19725  c1lip3  19844  lhop  19861  dvcnvrelem1  19862  mdegfval  19946  aalioulem3  20212  taylthlem2  20251  efifo  20410  dfrelog  20424  efopnlem2  20509  xrlimcnp  20768  fsumdvdsmul  20941  dchrghm  21001  usgrares1  21385  cusgrares  21442  ex-ima  21711  subgornss  21855  efghgrp  21922  imadifxp  23999  mbfmcst  24570  0rrv  24670  cvmliftmolem1  24929  cvmlift2lem9a  24951  cvmlift2lem9  24959  rdgprc  25373  dfrdg2  25374  dfon4  25655  ivthALT  26236  cnres2  26370  imaiinfv  26638  diophrw  26715  dnnumch1  27017  fnwe2lem2  27024  lindsmm  27174  hbtlem6  27209  funcoressn  27866  hashimarn  28002  csbima12gALTVD  28727  diaintclN  31553  dibintclN  31662  dihintcl  31839
  Copyright terms: Public domain W3C validator