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

Definition df-ima 4682
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 20772). Contrast with restriction (df-res 4681) and range (df-rn 4680). For an alternate definition, see dfima2 5002. (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 4664 . 2  class  ( A
" B )
41, 2cres 4663 . . 3  class  ( A  |`  B )
54crn 4662 . 2  class  ran  (  A  |`  B )
63, 5wceq 1619 1  wff  ( A
" B )  =  ran  (  A  |`  B )
Colors of variables: wff set class
This definition is referenced by:  resima  4975  resima2  4976  imaeq1  4995  imaeq2  4996  dfima2  5002  nfima  5008  csbima12gALT  5011  rnresi  5016  resiima  5017  ima0  5018  imadisj  5020  imass1  5036  imass2  5037  ndmima  5038  imaundi  5081  imaundir  5082  rninxp  5105  imainrect  5107  dfrn4  5121  imacnvcnv  5124  imadmres  5152  mptpreima  5153  rnco2  5167  funcnvres  5259  funimacnv  5262  fnima  5300  fores  5398  f1ores  5425  f1orescnv  5426  foimacnv  5428  resdif  5432  fvres  5475  resfunexgALT  5672  funfvima  5687  funiunfv  5708  soisores  5758  curry1  6144  curry2  6147  fparlem3  6154  fparlem4  6155  smores2  6339  tz7.44-3  6389  tz7.49c  6426  seqomlem2  6431  seqomlem3  6432  seqomlem4  6433  sbthlem4  6942  sbthlem6  6944  sbthlem8  6946  fodomfi  7103  dffi3  7152  marypha1lem  7154  marypha2lem4  7159  dfsup3OLD  7165  ordtypelem3  7203  ordtypelem9  7209  wdomima2g  7268  rankwflemb  7433  dfac8alem  7624  dfac12lem1  7737  zorn2lem1  8091  ttukeylem3  8106  imadomg  8127  iunfo  8129  fpwwe2lem6  8225  fpwwe2lem9  8228  fpwwe2lem13  8232  gruima  8392  peano5nni  9717  1nn  9725  peano2nn  9726  seqval  11023  hashf1lem1  11358  frmdss2  14447  ghmima  14665  conjsubg  14676  gsumzaddlem  15165  gsumxp  15189  dprd2da  15239  dmdprdsplit2lem  15242  ablfac1b  15267  mplsubrglem  16145  pjdm  16569  tgrest  16852  cnconst2  16973  imacmp  17086  cmpfi  17097  conima  17113  kgencn3  17215  ptpjopn  17268  xkoccn  17275  txkgen  17308  qtoprest  17370  hmeores  17424  txflf  17663  subgntr  17751  opnsubg  17752  clsnsg  17754  tgpconcomp  17757  snclseqg  17760  tsmsf1o  17789  tsmsxplem1  17797  ovolicc2lem4  18841  mbflimsup  18983  itg1addlem4  19016  ellimc2  19189  c1lip3  19308  lhop  19325  dvcnvrelem1  19326  mdegfval  19410  aalioulem3  19676  taylthlem2  19715  efifo  19871  dfrelog  19885  efopnlem2  19966  xrlimcnp  20225  fsumdvdsmul  20397  dchrghm  20457  ex-ima  20772  subgornss  20933  efghgrp  21000  cvmliftmolem1  23184  cvmlift2lem9a  23206  cvmlift2lem9  23214  rdgprc  23520  dfrdg2  23521  dfon4  23809  domrancur1b  24567  domrancur1c  24569  prsubrtr  24766  ivthALT  25625  cnres2  25850  imaiinfv  26126  diophrw  26205  dnnumch1  26508  fnwe2lem2  26515  lindsmm  26665  hbtlem6  26700  csbima12gALTVD  27723  diaintclN  30415  dibintclN  30524  dihintcl  30701
  Copyright terms: Public domain W3C validator