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

Definition df-ima 4857
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 22259). Contrast with restriction (df-res 4856) and range (df-rn 4855). For an alternate definition, see dfima2 5173. (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 4847 . 2
41, 2cres 4846 . . 3
54crn 4845 . 2
63, 5wceq 1662 1
Colors of variables: wff set class
This definition is referenced by:  resima  5147  resima2  5148  imaeq1  5166  imaeq2  5167  dfima2  5173  nfima  5179  rnresi  5184  resiima  5185  ima0  5186  imadisj  5190  imass1  5205  imass2  5206  ndmima  5207  imaundi  5250  imaundir  5251  inimass  5254  rninxp  5277  imainrect  5279  xpima  5280  dfrn4  5297  imacnvcnv  5302  imadmres  5329  mptpreima  5330  rnco2  5344  funcnvres  5484  funimacnv  5487  fnima  5526  fores  5623  f1ores  5649  f1orescnv  5650  foimacnv  5652  resdif  5655  funfvima  5930  funiunfv  5943  soisores  5992  resfunexgALT  6502  curry1  6621  curry2  6624  fparlem3  6631  fparlem4  6632  smores2  6728  tz7.44-3  6778  tz7.49c  6815  seqomlem2  6820  seqomlem3  6821  seqomlem4  6822  sbthlem4  7332  sbthlem6  7334  sbthlem8  7336  fodomfi  7497  dffi3  7548  marypha1lem  7550  marypha2lem4  7555  dfsup3OLD  7561  ordtypelem3  7601  ordtypelem9  7607  wdomima2g  7666  rankwflemb  7831  dfac8alem  8024  dfac12lem1  8137  zorn2lem1  8490  ttukeylem3  8505  imadomg  8526  iunfo  8528  fpwwe2lem6  8624  fpwwe2lem9  8627  fpwwe2lem13  8631  gruima  8791  peano5nni  10134  1nn  10142  peano2nn  10143  seqval  11609  hashimarn  11987  hashf1lem1  11995  frmdss2  15311  ghmima  15529  conjsubg  15540  gsumzaddlem  16029  gsumxp  16053  dprd2da  16103  dmdprdsplit2lem  16106  ablfac1b  16131  mplsubrglem  17005  pjdm  17437  tgrest  17726  cnconst2  17850  imacmp  17963  cmpfi  17974  conima  17992  kgencn3  18094  ptpjopn  18148  xkoccn  18155  txkgen  18188  qtoprest  18253  hmeores  18307  txflf  18542  subgntr  18640  opnsubg  18641  clsnsg  18643  tgpconcomp  18646  snclseqg  18649  tsmsf1o  18678  tsmsxplem1  18686  fmucndlem  18825  ovolicc2lem4  19920  mbflimsup  20060  itg1addlem4  20093  ellimc2  20268  c1lip3  20387  lhop  20404  dvcnvrelem1  20405  mdegfval  20489  aalioulem3  20755  taylthlem2  20794  efifo  20958  dfrelog  20972  efopnlem2  21057  xrlimcnp  21316  fsumdvdsmul  21489  dchrghm  21549  usgrares1  21933  cusgrares  21990  ex-ima  22259  subgornss  22403  efghgrp  22470  imadifxp  24558  ffsrn  24650  mbfmcst  25345  0rrv  25475  cvmliftmolem1  25807  cvmlift2lem9a  25829  cvmlift2lem9  25837  rdgprc  26252  dfrdg2  26253  dfon4  26568  ivthALT  27201  cnres2  27335  imaiinfv  27671  diophrw  27748  dnnumch1  28048  fnwe2lem2  28055  lindsmm  28204  hbtlem6  28239  funcoressn  28889  fvelrnfvelrnressn  29010  csbima12gALTOLD  30128  csbima12gALTVD  30202  diaintclN  33129  dibintclN  33238  dihintcl  33415
  Copyright terms: Public domain W3C validator