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

Definition df-ima 4824
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 23328). Contrast with restriction (df-res 4823) and range (df-rn 4822). For an alternate definition, see dfima2 5143. (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 4814 . 2
41, 2cres 4813 . . 3
54crn 4812 . 2
63, 5wceq 1687 1
Colors of variables: wff setvar class
This definition is referenced by:  resima  5114  resima2  5115  imaeq1  5136  imaeq2  5137  dfima2  5143  nfima  5149  rnresi  5154  resiima  5155  ima0  5156  imadisj  5160  imass1  5175  imass2  5176  ndmima  5177  imaundi  5221  imaundir  5222  inimass  5225  rninxp  5249  imainrect  5251  xpima  5252  dfrn4  5270  imacnvcnv  5275  imadmres  5302  mptpreima  5303  rnco2  5317  funcnvres  5457  funimacnv  5460  fnima  5499  fores  5599  f1ores  5625  f1orescnv  5626  foimacnv  5628  resdif  5631  funfvima  5920  funiunfv  5933  soisores  5986  resfunexgALT  6509  curry1  6633  curry2  6636  fparlem3  6643  fparlem4  6644  smores2  6774  tz7.44-3  6823  tz7.49c  6860  seqomlem2  6865  seqomlem3  6866  seqomlem4  6867  sbthlem4  7383  sbthlem6  7385  sbthlem8  7387  fodomfi  7549  dffi3  7628  marypha1lem  7630  marypha2lem4  7635  dfsup3OLD  7641  ordtypelem3  7681  ordtypelem9  7687  wdomima2g  7748  rankwflemb  7947  dfac8alem  8146  dfac12lem1  8259  zorn2lem1  8612  ttukeylem3  8627  imadomg  8648  iunfo  8650  fpwwe2lem6  8748  fpwwe2lem9  8751  fpwwe2lem13  8755  gruima  8915  peano5nni  10271  1nn  10279  peano2nn  10280  seqval  11758  hashimarn  12141  hashf1lem1  12149  frmdss2  15478  ghmima  15704  conjsubg  15715  gsumzaddlem  16329  gsumxp  16359  dprd2da  16409  dmdprdsplit2lem  16412  ablfac1b  16437  mplsubrglem  17325  pjdm  17840  lindsmm  17956  tgrest  18467  cnconst2  18591  imacmp  18704  cmpfi  18715  conima  18733  kgencn3  18835  ptpjopn  18889  xkoccn  18896  txkgen  18929  qtoprest  18994  hmeores  19048  txflf  19283  subgntr  19381  opnsubg  19382  clsnsg  19384  tgpconcomp  19387  snclseqg  19390  tsmsf1o  19419  tsmsxplem1  19427  fmucndlem  19566  ovolicc2lem4  20703  mbflimsup  20844  itg1addlem4  20877  ellimc2  21052  c1lip3  21171  lhop  21188  dvcnvrelem1  21189  mdegfval  21273  aalioulem3  21541  taylthlem2  21580  efifo  21744  dfrelog  21758  efopnlem2  21843  xrlimcnp  22103  fsumdvdsmul  22276  dchrghm  22336  usgrares1  23002  cusgrares  23059  ex-ima  23328  subgornss  23472  efghgrp  23539  imadifxp  25619  ffsrn  25709  mbfmcst  26383  0rrv  26537  cvmliftmolem1  26873  cvmlift2lem9a  26895  cvmlift2lem9  26903  rdgprc  27310  dfrdg2  27311  dfon4  27626  ivthALT  28201  cnres2  28333  imaiinfv  28701  diophrw  28770  dnnumch1  29070  fnwe2lem2  29077  hbtlem6  29158  funcoressn  29707  fvelrnfvelrnressn  29825  gsumXzaddlem  30478  gsumXxp  30508  csbima12gALTOLD  31136  csbima12gALTVD  31211  diaintclN  34140  dibintclN  34249  dihintcl  34426
  Copyright terms: Public domain W3C validator