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

Definition df-ima 4852
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 25971). Contrast with restriction (df-res 4851) and range (df-rn 4850). For an alternate definition, see dfima2 5176. (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 4842 . 2  class  ( A
" B )
41, 2cres 4841 . . 3  class  ( A  |`  B )
54crn 4840 . 2  class  ran  ( A  |`  B )
63, 5wceq 1452 1  wff  ( A
" B )  =  ran  ( A  |`  B )
Colors of variables: wff setvar class
This definition is referenced by:  resima  5143  resima2  5144  imaeq1  5169  imaeq2  5170  dfima2  5176  nfima  5182  rnresi  5187  resiima  5188  ima0  5189  imadisj  5193  imass1  5209  imass2  5210  ndmimaOLD  5212  imaundi  5254  imaundir  5255  inimass  5258  rninxp  5282  imainrect  5284  xpima  5285  dfrn4  5303  imacnvcnv  5307  imadmres  5334  mptpreima  5335  rnco2  5349  funcnvres  5662  funimacnv  5665  fnima  5704  fores  5815  f1ores  5842  f1orescnv  5843  foimacnv  5845  resdif  5848  fvrnressn  6095  funfvima  6157  funiunfv  6171  soisores  6236  resfunexgALT  6775  curry1  6907  curry2  6910  fparlem3  6917  fparlem4  6918  smores2  7091  tz7.44-3  7144  tz7.49c  7181  seqomlem2  7186  seqomlem3  7187  seqomlem4  7188  sbthlem4  7703  sbthlem6  7705  sbthlem8  7707  fodomfi  7868  dffi3  7963  marypha1lem  7965  marypha2lem4  7970  ordtypelem3  8053  ordtypelem9  8059  wdomima2g  8119  rankwflemb  8282  dfac8alem  8478  dfac12lem1  8591  zorn2lem1  8944  ttukeylem3  8959  imadomg  8980  iunfo  8982  fpwwe2lem6  9078  fpwwe2lem9  9081  fpwwe2lem13  9085  gruima  9245  peano5nni  10634  1nn  10642  peano2nn  10643  seqval  12262  hashimarn  12651  hashf1lem1  12659  frmdss2  16725  ghmima  16981  conjsubg  16992  gsumzaddlem  17632  gsumxp  17686  dprd2da  17753  dmdprdsplit2lem  17756  ablfac1b  17781  mplsubrglem  18740  pjdm  19347  lindsmm  19463  tgrest  20252  cnconst2  20376  imacmp  20489  cmpfi  20500  conima  20517  kgencn3  20650  ptpjopn  20704  xkoccn  20711  txkgen  20744  qtoprest  20809  hmeores  20863  txflf  21099  subgntr  21199  opnsubg  21200  clsnsg  21202  tgpconcomp  21205  snclseqg  21208  tsmsf1o  21237  tsmsxplem1  21245  fmucndlem  21384  ovolicc2lem4OLD  22551  ovolicc2lem4  22552  mbflimsup  22702  mbflimsupOLD  22703  itg1addlem4  22736  ellimc2  22911  c1lip3  23030  lhop  23047  dvcnvrelem1  23048  mdegfval  23090  aalioulem3  23369  taylthlem2  23408  efifo  23575  dfrelog  23594  efopnlem2  23681  xrlimcnp  23973  fsumdvdsmul  24203  dchrghm  24263  usgrares1  25217  cusgrares  25279  ex-ima  25971  subgornss  26115  efghgrpOLD  26182  imadifxp  28288  fresf1o  28307  imafi2  28367  ffsrn  28389  mbfmcst  29154  0rrv  29357  cvmliftmolem1  30076  cvmlift2lem9a  30098  cvmlift2lem9  30106  mrsubff1o  30225  msubff1o  30267  rdgprc  30512  dfrdg2  30513  dfon4  30731  ivthALT  31062  mptsnunlem  31810  dissneqlem  31812  icoreelrnab  31827  icoreunrn  31832  poimirlem3  32007  poimirlem9  32013  poimirlem16  32020  poimirlem19  32023  poimirlem30  32034  cnres2  32159  diaintclN  34697  dibintclN  34806  dihintcl  34983  imaiinfv  35606  diophrw  35672  dnnumch1  35973  fnwe2lem2  35980  hbtlem6  36059  imanonrel  36270  rp-imass  36437  csbima12gALTOLD  37281  csbima12gALTVD  37357  funcoressn  38773  uhgrspan1  39539
  Copyright terms: Public domain W3C validator