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

Definition df-ima 5017
Description: Define the image of a class (as restricted by another class). Definition 6.6(2) of [TakeutiZaring] p. 24. For example, ->( " )={6} (ex-ima 25163). Contrast with restriction (df-res 5016) and range (df-rn 5015). For an alternate definition, see dfima2 5344. (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 5007 . 2
41, 2cres 5006 . . 3
54crn 5005 . 2
63, 5wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  resima  5311  resima2  5312  imaeq1  5337  imaeq2  5338  dfima2  5344  nfima  5350  rnresi  5355  resiima  5356  ima0  5357  imadisj  5361  imass1  5376  imass2  5377  ndmima  5378  imaundi  5423  imaundir  5424  inimass  5427  rninxp  5451  imainrect  5453  xpima  5454  dfrn4  5472  imacnvcnv  5477  imadmres  5504  mptpreima  5505  rnco2  5519  funcnvres  5662  funimacnv  5665  fnima  5704  fores  5809  f1ores  5835  f1orescnv  5836  foimacnv  5838  resdif  5841  fvrnressn  6086  funfvima  6147  funiunfv  6160  soisores  6223  resfunexgALT  6763  curry1  6892  curry2  6895  fparlem3  6902  fparlem4  6903  smores2  7044  tz7.44-3  7093  tz7.49c  7130  seqomlem2  7135  seqomlem3  7136  seqomlem4  7137  sbthlem4  7650  sbthlem6  7652  sbthlem8  7654  fodomfi  7819  dffi3  7911  marypha1lem  7913  marypha2lem4  7918  dfsup3OLD  7924  ordtypelem3  7966  ordtypelem9  7972  wdomima2g  8033  rankwflemb  8232  dfac8alem  8431  dfac12lem1  8544  zorn2lem1  8897  ttukeylem3  8912  imadomg  8933  iunfo  8935  fpwwe2lem6  9034  fpwwe2lem9  9037  fpwwe2lem13  9041  gruima  9201  peano5nni  10564  1nn  10572  peano2nn  10573  seqval  12118  hashimarn  12496  hashf1lem1  12504  frmdss2  16031  ghmima  16287  conjsubg  16298  gsumzaddlem  16934  gsumzaddlemOLD  16936  gsumxp  17004  gsumxpOLD  17006  dprd2da  17091  dmdprdsplit2lem  17094  ablfac1b  17121  mplsubrglem  18100  mplsubrglemOLD  18101  pjdm  18738  lindsmm  18863  tgrest  19660  cnconst2  19784  imacmp  19897  cmpfi  19908  conima  19926  kgencn3  20059  ptpjopn  20113  xkoccn  20120  txkgen  20153  qtoprest  20218  hmeores  20272  txflf  20507  subgntr  20605  opnsubg  20606  clsnsg  20608  tgpconcomp  20611  snclseqg  20614  tsmsf1o  20647  tsmsxplem1  20655  fmucndlem  20794  ovolicc2lem4  21931  mbflimsup  22073  itg1addlem4  22106  ellimc2  22281  c1lip3  22400  lhop  22417  dvcnvrelem1  22418  mdegfval  22460  aalioulem3  22730  taylthlem2  22769  efifo  22934  dfrelog  22953  efopnlem2  23038  xrlimcnp  23298  fsumdvdsmul  23471  dchrghm  23531  usgrares1  24410  cusgrares  24472  ex-ima  25163  subgornss  25308  efghgrpOLD  25375  imadifxp  27458  ffsrn  27552  mbfmcst  28230  0rrv  28390  cvmliftmolem1  28726  cvmlift2lem9a  28748  cvmlift2lem9  28756  mrsubff1o  28875  msubff1o  28917  rdgprc  29227  dfrdg2  29228  dfon4  29543  ivthALT  30153  cnres2  30259  imaiinfv  30625  diophrw  30692  dnnumch1  30990  fnwe2lem2  30997  hbtlem6  31078  funcoressn  32212  csbima12gALTOLD  33622  csbima12gALTVD  33697  diaintclN  36785  dibintclN  36894  dihintcl  37071  rp-imass  37795
  Copyright terms: Public domain W3C validator