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

Definition df-ima 4702
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 20829). Contrast with restriction (df-res 4701) and range (df-rn 4700). For an alternate definition, see dfima2 5014. (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 4692 . 2  class  ( A
" B )
41, 2cres 4691 . . 3  class  ( A  |`  B )
54crn 4690 . 2  class  ran  ( A  |`  B )
63, 5wceq 1623 1  wff  ( A
" B )  =  ran  ( A  |`  B )
Colors of variables: wff set class
This definition is referenced by:  resima  4987  resima2  4988  imaeq1  5007  imaeq2  5008  dfima2  5014  nfima  5020  csbima12gALT  5023  rnresi  5028  resiima  5029  ima0  5030  imadisj  5032  imass1  5048  imass2  5049  ndmima  5050  imaundi  5093  imaundir  5094  rninxp  5117  imainrect  5119  dfrn4  5134  imacnvcnv  5137  imadmres  5165  mptpreima  5166  rnco2  5180  funcnvres  5321  funimacnv  5324  fnima  5362  fores  5460  f1ores  5487  f1orescnv  5488  foimacnv  5490  resdif  5494  resfunexgALT  5738  funfvima  5753  funiunfv  5774  soisores  5824  curry1  6210  curry2  6213  fparlem3  6220  fparlem4  6221  smores2  6371  tz7.44-3  6421  tz7.49c  6458  seqomlem2  6463  seqomlem3  6464  seqomlem4  6465  sbthlem4  6974  sbthlem6  6976  sbthlem8  6978  fodomfi  7135  dffi3  7184  marypha1lem  7186  marypha2lem4  7191  dfsup3OLD  7197  ordtypelem3  7235  ordtypelem9  7241  wdomima2g  7300  rankwflemb  7465  dfac8alem  7656  dfac12lem1  7769  zorn2lem1  8123  ttukeylem3  8138  imadomg  8159  iunfo  8161  fpwwe2lem6  8257  fpwwe2lem9  8260  fpwwe2lem13  8264  gruima  8424  peano5nni  9749  1nn  9757  peano2nn  9758  seqval  11057  hashf1lem1  11393  frmdss2  14485  ghmima  14703  conjsubg  14714  gsumzaddlem  15203  gsumxp  15227  dprd2da  15277  dmdprdsplit2lem  15280  ablfac1b  15305  mplsubrglem  16183  pjdm  16607  tgrest  16890  cnconst2  17011  imacmp  17124  cmpfi  17135  conima  17151  kgencn3  17253  ptpjopn  17306  xkoccn  17313  txkgen  17346  qtoprest  17408  hmeores  17462  txflf  17701  subgntr  17789  opnsubg  17790  clsnsg  17792  tgpconcomp  17795  snclseqg  17798  tsmsf1o  17827  tsmsxplem1  17835  ovolicc2lem4  18879  mbflimsup  19021  itg1addlem4  19054  ellimc2  19227  c1lip3  19346  lhop  19363  dvcnvrelem1  19364  mdegfval  19448  aalioulem3  19714  taylthlem2  19753  efifo  19909  dfrelog  19923  efopnlem2  20004  xrlimcnp  20263  fsumdvdsmul  20435  dchrghm  20495  ex-ima  20829  subgornss  20973  efghgrp  21040  xpima  23202  mbfmcst  23564  0rrv  23654  cvmliftmolem1  23812  cvmlift2lem9a  23834  cvmlift2lem9  23842  rdgprc  24151  dfrdg2  24152  dfon4  24433  domrancur1b  25200  domrancur1c  25202  prsubrtr  25399  ivthALT  26258  cnres2  26483  imaiinfv  26759  diophrw  26838  dnnumch1  27141  fnwe2lem2  27148  lindsmm  27298  hbtlem6  27333  funcoressn  27990  csbima12gALTVD  28673  diaintclN  31248  dibintclN  31357  dihintcl  31534
  Copyright terms: Public domain W3C validator