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 5051
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 26691). Contrast with restriction (df-res 5050) and range (df-rn 5049). For an alternate definition, see dfima2 5387. (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 5041 . 2 class (𝐴𝐵)
41, 2cres 5040 . . 3 class (𝐴𝐵)
54crn 5039 . 2 class ran (𝐴𝐵)
63, 5wceq 1475 1 wff (𝐴𝐵) = ran (𝐴𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  resima  5351  resima2  5352  resima2OLD  5353  imaeq1  5380  imaeq2  5381  dfima2  5387  nfima  5393  rnresi  5398  resiima  5399  ima0  5400  imadisj  5403  imass1  5419  imass2  5420  imaundi  5464  imaundir  5465  inimass  5468  rninxp  5492  imainrect  5494  xpima  5495  dfrn4  5513  imacnvcnv  5517  imadmres  5544  mptpreima  5545  rnco2  5559  funcnvres  5881  funimacnv  5884  fnima  5923  fores  6037  f1ores  6064  f1orescnv  6065  foimacnv  6067  resdif  6070  fvrnressn  6333  funfvima  6396  funiunfv  6410  soisores  6477  resfunexgALT  7022  curry1  7156  curry2  7159  fparlem3  7166  fparlem4  7167  smores2  7338  tz7.44-3  7391  tz7.49c  7428  seqomlem2  7433  seqomlem3  7434  seqomlem4  7435  sbthlem4  7958  sbthlem6  7960  sbthlem8  7962  fodomfi  8124  dffi3  8220  marypha1lem  8222  marypha2lem4  8227  ordtypelem3  8308  ordtypelem9  8314  wdomima2g  8374  rankwflemb  8539  dfac8alem  8735  dfac12lem1  8848  zorn2lem1  9201  ttukeylem3  9216  imadomg  9237  iunfo  9240  fpwwe2lem6  9336  fpwwe2lem9  9339  fpwwe2lem13  9343  gruima  9503  peano5nni  10900  1nn  10908  peano2nn  10909  seqval  12674  hashimarn  13085  hashf1lem1  13096  frmdss2  17223  ghmima  17504  conjsubg  17515  gsumzaddlem  18144  gsumxp  18198  dprd2da  18264  dmdprdsplit2lem  18267  ablfac1b  18292  mplsubrglem  19260  pjdm  19870  lindsmm  19986  tgrest  20773  cnconst2  20897  imacmp  21010  cmpfi  21021  conima  21038  kgencn3  21171  ptpjopn  21225  xkoccn  21232  txkgen  21265  qtoprest  21330  hmeores  21384  txflf  21620  subgntr  21720  opnsubg  21721  clsnsg  21723  tgpconcomp  21726  snclseqg  21729  tsmsf1o  21758  tsmsxplem1  21766  fmucndlem  21905  ovolicc2lem4  23095  mbflimsup  23239  itg1addlem4  23272  ellimc2  23447  c1lip3  23566  lhop  23583  dvcnvrelem1  23584  mdegfval  23626  aalioulem3  23893  taylthlem2  23932  efifo  24097  dfrelog  24116  efopnlem2  24203  xrlimcnp  24495  fsumdvdsmul  24721  dchrghm  24781  usgrares1  25939  cusgrares  26001  ex-ima  26691  imadifxp  28796  fresf1o  28815  imafi2  28872  ffsrn  28892  mbfmcst  29648  0rrv  29840  cvmliftmolem1  30517  cvmlift2lem9a  30539  cvmlift2lem9  30547  mrsubff1o  30666  msubff1o  30708  rdgprc  30944  dfrdg2  30945  dfon4  31170  ivthALT  31500  mptsnunlem  32361  dissneqlem  32363  icoreelrnab  32378  icoreunrn  32383  poimirlem3  32582  poimirlem9  32588  poimirlem16  32595  poimirlem19  32598  poimirlem30  32609  cnres2  32732  diaintclN  35365  dibintclN  35474  dihintcl  35651  imaiinfv  36274  diophrw  36340  dnnumch1  36632  fnwe2lem2  36639  hbtlem6  36718  imanonrel  36918  rp-imass  37085  csbima12gALTOLD  38079  csbima12gALTVD  38155  funcoressn  39856  uhgrspan1  40527
  Copyright terms: Public domain W3C validator