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 4847
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 25892). Contrast with restriction (df-res 4846) and range (df-rn 4845). For an alternate definition, see dfima2 5170. (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 4837 . 2  class  ( A
" B )
41, 2cres 4836 . . 3  class  ( A  |`  B )
54crn 4835 . 2  class  ran  ( A  |`  B )
63, 5wceq 1444 1  wff  ( A
" B )  =  ran  ( A  |`  B )
Colors of variables: wff setvar class
This definition is referenced by:  resima  5137  resima2  5138  imaeq1  5163  imaeq2  5164  dfima2  5170  nfima  5176  rnresi  5181  resiima  5182  ima0  5183  imadisj  5187  imass1  5203  imass2  5204  ndmimaOLD  5206  imaundi  5248  imaundir  5249  inimass  5252  rninxp  5276  imainrect  5278  xpima  5279  dfrn4  5296  imacnvcnv  5300  imadmres  5327  mptpreima  5328  rnco2  5342  funcnvres  5652  funimacnv  5655  fnima  5694  fores  5802  f1ores  5828  f1orescnv  5829  foimacnv  5831  resdif  5834  fvrnressn  6079  funfvima  6140  funiunfv  6153  soisores  6218  resfunexgALT  6756  curry1  6888  curry2  6891  fparlem3  6898  fparlem4  6899  smores2  7073  tz7.44-3  7126  tz7.49c  7163  seqomlem2  7168  seqomlem3  7169  seqomlem4  7170  sbthlem4  7685  sbthlem6  7687  sbthlem8  7689  fodomfi  7850  dffi3  7945  marypha1lem  7947  marypha2lem4  7952  ordtypelem3  8035  ordtypelem9  8041  wdomima2g  8101  rankwflemb  8264  dfac8alem  8460  dfac12lem1  8573  zorn2lem1  8926  ttukeylem3  8941  imadomg  8962  iunfo  8964  fpwwe2lem6  9060  fpwwe2lem9  9063  fpwwe2lem13  9067  gruima  9227  peano5nni  10612  1nn  10620  peano2nn  10621  seqval  12224  hashimarn  12610  hashf1lem1  12618  frmdss2  16647  ghmima  16903  conjsubg  16914  gsumzaddlem  17554  gsumxp  17608  dprd2da  17675  dmdprdsplit2lem  17678  ablfac1b  17703  mplsubrglem  18663  pjdm  19270  lindsmm  19386  tgrest  20175  cnconst2  20299  imacmp  20412  cmpfi  20423  conima  20440  kgencn3  20573  ptpjopn  20627  xkoccn  20634  txkgen  20667  qtoprest  20732  hmeores  20786  txflf  21021  subgntr  21121  opnsubg  21122  clsnsg  21124  tgpconcomp  21127  snclseqg  21130  tsmsf1o  21159  tsmsxplem1  21167  fmucndlem  21306  ovolicc2lem4OLD  22473  ovolicc2lem4  22474  mbflimsup  22623  mbflimsupOLD  22624  itg1addlem4  22657  ellimc2  22832  c1lip3  22951  lhop  22968  dvcnvrelem1  22969  mdegfval  23011  aalioulem3  23290  taylthlem2  23329  efifo  23496  dfrelog  23515  efopnlem2  23602  xrlimcnp  23894  fsumdvdsmul  24124  dchrghm  24184  usgrares1  25138  cusgrares  25200  ex-ima  25892  subgornss  26034  efghgrpOLD  26101  imadifxp  28212  fresf1o  28231  imafi2  28292  ffsrn  28314  mbfmcst  29081  0rrv  29284  cvmliftmolem1  30004  cvmlift2lem9a  30026  cvmlift2lem9  30034  mrsubff1o  30153  msubff1o  30195  rdgprc  30441  dfrdg2  30442  dfon4  30660  ivthALT  30991  mptsnunlem  31740  dissneqlem  31742  icoreelrnab  31757  icoreunrn  31762  poimirlem3  31943  poimirlem9  31949  poimirlem16  31956  poimirlem19  31959  poimirlem30  31970  cnres2  32095  diaintclN  34626  dibintclN  34735  dihintcl  34912  imaiinfv  35535  diophrw  35601  dnnumch1  35902  fnwe2lem2  35909  hbtlem6  35988  imanonrel  36199  rp-imass  36366  csbima12gALTOLD  37218  csbima12gALTVD  37294  funcoressn  38628  uhgrspan1  39375
  Copyright terms: Public domain W3C validator