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

Definition df-ima 4875
Description: Define the image of a class (as restricted by another class). Definition 6.6(2) of [TakeutiZaring] p. 24. For example, ( ={<.2,6>.,<.3,9>.}/\B={1,2})->( "B)={6} (ex-ima 22771). Contrast with restriction (df-res 4874) and range (df-rn 4873). For an alternate definition, see dfima2 5194. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
df-ima

Detailed syntax breakdown of Definition df-ima
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2cima 4865 . 2
41, 2cres 4864 . . 3
54crn 4863 . 2
63, 5wceq 1670 1
Colors of variables: wff set class
This definition is referenced by:  resima  5165  resima2  5166  imaeq1  5187  imaeq2  5188  dfima2  5194  nfima  5200  rnresi  5205  resiima  5206  ima0  5207  imadisj  5211  imass1  5226  imass2  5227  ndmima  5228  imaundi  5271  imaundir  5272  inimass  5275  rninxp  5298  imainrect  5300  xpima  5301  dfrn4  5318  imacnvcnv  5323  imadmres  5350  mptpreima  5351  rnco2  5365  funcnvres  5505  funimacnv  5508  fnima  5547  fores  5646  f1ores  5672  f1orescnv  5673  foimacnv  5675  resdif  5678  funfvima  5966  funiunfv  5979  soisores  6028  resfunexgALT  6547  curry1  6670  curry2  6673  fparlem3  6680  fparlem4  6681  smores2  6778  tz7.44-3  6828  tz7.49c  6865  seqomlem2  6870  seqomlem3  6871  seqomlem4  6872  sbthlem4  7385  sbthlem6  7387  sbthlem8  7389  fodomfi  7551  dffi3  7603  marypha1lem  7605  marypha2lem4  7610  dfsup3OLD  7616  ordtypelem3  7656  ordtypelem9  7662  wdomima2g  7721  rankwflemb  7886  dfac8alem  8081  dfac12lem1  8194  zorn2lem1  8547  ttukeylem3  8562  imadomg  8583  iunfo  8585  fpwwe2lem6  8681  fpwwe2lem9  8684  fpwwe2lem13  8688  gruima  8848  peano5nni  10191  1nn  10199  peano2nn  10200  seqval  11666  hashimarn  12047  hashf1lem1  12055  frmdss2  15379  ghmima  15597  conjsubg  15608  gsumzaddlem  16136  gsumxp  16165  dprd2da  16215  dmdprdsplit2lem  16218  ablfac1b  16243  mplsubrglem  17127  pjdm  17559  tgrest  18237  cnconst2  18361  imacmp  18474  cmpfi  18485  conima  18503  kgencn3  18605  ptpjopn  18659  xkoccn  18666  txkgen  18699  qtoprest  18764  hmeores  18818  txflf  19053  subgntr  19151  opnsubg  19152  clsnsg  19154  tgpconcomp  19157  snclseqg  19160  tsmsf1o  19189  tsmsxplem1  19197  fmucndlem  19336  ovolicc2lem4  20431  mbflimsup  20571  itg1addlem4  20604  ellimc2  20779  c1lip3  20898  lhop  20915  dvcnvrelem1  20916  mdegfval  21000  aalioulem3  21266  taylthlem2  21305  efifo  21469  dfrelog  21483  efopnlem2  21568  xrlimcnp  21828  fsumdvdsmul  22001  dchrghm  22061  usgrares1  22445  cusgrares  22502  ex-ima  22771  subgornss  22915  efghgrp  22982  imadifxp  25067  ffsrn  25159  mbfmcst  25854  0rrv  25984  cvmliftmolem1  26316  cvmlift2lem9a  26338  cvmlift2lem9  26346  rdgprc  26761  dfrdg2  26762  dfon4  27077  ivthALT  27710  cnres2  27844  imaiinfv  28174  diophrw  28245  dnnumch1  28545  fnwe2lem2  28552  lindsmm  28638  hbtlem6  28673  funcoressn  29212  fvelrnfvelrnressn  29332  csbima12gALTOLD  30405  csbima12gALTVD  30479  diaintclN  33406  dibintclN  33515  dihintcl  33692
  Copyright terms: Public domain W3C validator