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

Definition df-ima 4892
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 21751). Contrast with restriction (df-res 4891) and range (df-rn 4890). For an alternate definition, see dfima2 5206. (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 4882 . 2  class  ( A
" B )
41, 2cres 4881 . . 3  class  ( A  |`  B )
54crn 4880 . 2  class  ran  ( A  |`  B )
63, 5wceq 1653 1  wff  ( A
" B )  =  ran  ( A  |`  B )
Colors of variables: wff set class
This definition is referenced by:  resima  5179  resima2  5180  imaeq1  5199  imaeq2  5200  dfima2  5206  nfima  5212  csbima12gALT  5215  rnresi  5220  resiima  5221  ima0  5222  imadisj  5224  imass1  5240  imass2  5241  ndmima  5242  imaundi  5285  imaundir  5286  inimass  5289  rninxp  5311  imainrect  5313  xpima  5314  dfrn4  5332  imacnvcnv  5335  imadmres  5363  mptpreima  5364  rnco2  5378  funcnvres  5523  funimacnv  5526  fnima  5564  fores  5663  f1ores  5690  f1orescnv  5691  foimacnv  5693  resdif  5697  resfunexgALT  5959  funfvima  5974  funiunfv  5996  soisores  6048  curry1  6439  curry2  6442  fparlem3  6449  fparlem4  6450  smores2  6617  tz7.44-3  6667  tz7.49c  6704  seqomlem2  6709  seqomlem3  6710  seqomlem4  6711  sbthlem4  7221  sbthlem6  7223  sbthlem8  7225  fodomfi  7386  dffi3  7437  marypha1lem  7439  marypha2lem4  7444  dfsup3OLD  7450  ordtypelem3  7490  ordtypelem9  7496  wdomima2g  7555  rankwflemb  7720  dfac8alem  7911  dfac12lem1  8024  zorn2lem1  8377  ttukeylem3  8392  imadomg  8413  iunfo  8415  fpwwe2lem6  8511  fpwwe2lem9  8514  fpwwe2lem13  8518  gruima  8678  peano5nni  10004  1nn  10012  peano2nn  10013  seqval  11335  hashf1lem1  11705  frmdss2  14809  ghmima  15027  conjsubg  15038  gsumzaddlem  15527  gsumxp  15551  dprd2da  15601  dmdprdsplit2lem  15604  ablfac1b  15629  mplsubrglem  16503  pjdm  16935  tgrest  17224  cnconst2  17348  imacmp  17461  cmpfi  17472  conima  17489  kgencn3  17591  ptpjopn  17645  xkoccn  17652  txkgen  17685  qtoprest  17750  hmeores  17804  txflf  18039  subgntr  18137  opnsubg  18138  clsnsg  18140  tgpconcomp  18143  snclseqg  18146  tsmsf1o  18175  tsmsxplem1  18183  fmucndlem  18322  ovolicc2lem4  19417  mbflimsup  19559  itg1addlem4  19592  ellimc2  19765  c1lip3  19884  lhop  19901  dvcnvrelem1  19902  mdegfval  19986  aalioulem3  20252  taylthlem2  20291  efifo  20450  dfrelog  20464  efopnlem2  20549  xrlimcnp  20808  fsumdvdsmul  20981  dchrghm  21041  usgrares1  21425  cusgrares  21482  ex-ima  21751  subgornss  21895  efghgrp  21962  imadifxp  24039  mbfmcst  24610  0rrv  24710  cvmliftmolem1  24969  cvmlift2lem9a  24991  cvmlift2lem9  24999  rdgprc  25423  dfrdg2  25424  dfon4  25739  ivthALT  26339  cnres2  26473  imaiinfv  26741  diophrw  26818  dnnumch1  27120  fnwe2lem2  27127  lindsmm  27276  hbtlem6  27311  funcoressn  27968  hashimarn  28164  csbima12gALTVD  29010  diaintclN  31857  dibintclN  31966  dihintcl  32143
  Copyright terms: Public domain W3C validator