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

Definition df-ima 5040
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⟩} ∧ 𝐵 = {1, 2}) → (𝐹𝐵) = {6} (ex-ima 26484). Contrast with restriction (df-res 5039) and range (df-rn 5038). For an alternate definition, see dfima2 5373. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
df-ima (𝐴𝐵) = ran (𝐴𝐵)

Detailed syntax breakdown of Definition df-ima
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2cima 5030 . 2 class (𝐴𝐵)
41, 2cres 5029 . . 3 class (𝐴𝐵)
54crn 5028 . 2 class ran (𝐴𝐵)
63, 5wceq 1474 1 wff (𝐴𝐵) = ran (𝐴𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  resima  5337  resima2  5338  resima2OLD  5339  imaeq1  5366  imaeq2  5367  dfima2  5373  nfima  5379  rnresi  5384  resiima  5385  ima0  5386  imadisj  5389  imass1  5405  imass2  5406  imaundi  5449  imaundir  5450  inimass  5453  rninxp  5477  imainrect  5479  xpima  5480  dfrn4  5498  imacnvcnv  5502  imadmres  5529  mptpreima  5530  rnco2  5544  funcnvres  5866  funimacnv  5869  fnima  5908  fores  6021  f1ores  6048  f1orescnv  6049  foimacnv  6051  resdif  6054  fvrnressn  6310  funfvima  6373  funiunfv  6387  soisores  6454  resfunexgALT  6999  curry1  7133  curry2  7136  fparlem3  7143  fparlem4  7144  smores2  7315  tz7.44-3  7368  tz7.49c  7405  seqomlem2  7410  seqomlem3  7411  seqomlem4  7412  sbthlem4  7935  sbthlem6  7937  sbthlem8  7939  fodomfi  8101  dffi3  8197  marypha1lem  8199  marypha2lem4  8204  ordtypelem3  8285  ordtypelem9  8291  wdomima2g  8351  rankwflemb  8516  dfac8alem  8712  dfac12lem1  8825  zorn2lem1  9178  ttukeylem3  9193  imadomg  9214  iunfo  9217  fpwwe2lem6  9313  fpwwe2lem9  9316  fpwwe2lem13  9320  gruima  9480  peano5nni  10872  1nn  10880  peano2nn  10881  seqval  12631  hashimarn  13039  hashf1lem1  13050  frmdss2  17171  ghmima  17452  conjsubg  17463  gsumzaddlem  18092  gsumxp  18146  dprd2da  18212  dmdprdsplit2lem  18215  ablfac1b  18240  mplsubrglem  19208  pjdm  19817  lindsmm  19933  tgrest  20720  cnconst2  20844  imacmp  20957  cmpfi  20968  conima  20985  kgencn3  21118  ptpjopn  21172  xkoccn  21179  txkgen  21212  qtoprest  21277  hmeores  21331  txflf  21567  subgntr  21667  opnsubg  21668  clsnsg  21670  tgpconcomp  21673  snclseqg  21676  tsmsf1o  21705  tsmsxplem1  21713  fmucndlem  21852  ovolicc2lem4  23039  mbflimsup  23183  itg1addlem4  23216  ellimc2  23391  c1lip3  23510  lhop  23527  dvcnvrelem1  23528  mdegfval  23570  aalioulem3  23837  taylthlem2  23876  efifo  24041  dfrelog  24060  efopnlem2  24147  xrlimcnp  24439  fsumdvdsmul  24665  dchrghm  24725  usgrares1  25732  cusgrares  25794  ex-ima  26484  imadifxp  28589  fresf1o  28608  imafi2  28665  ffsrn  28685  mbfmcst  29441  0rrv  29633  cvmliftmolem1  30310  cvmlift2lem9a  30332  cvmlift2lem9  30340  mrsubff1o  30459  msubff1o  30501  rdgprc  30737  dfrdg2  30738  dfon4  30963  ivthALT  31293  mptsnunlem  32144  dissneqlem  32146  icoreelrnab  32161  icoreunrn  32166  poimirlem3  32365  poimirlem9  32371  poimirlem16  32378  poimirlem19  32381  poimirlem30  32392  cnres2  32515  diaintclN  35148  dibintclN  35257  dihintcl  35434  imaiinfv  36057  diophrw  36123  dnnumch1  36415  fnwe2lem2  36422  hbtlem6  36501  imanonrel  36701  rp-imass  36868  csbima12gALTOLD  37862  csbima12gALTVD  37938  funcoressn  39639  uhgrspan1  40508
  Copyright terms: Public domain W3C validator