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 5324
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 27626). Contrast with restriction (df-res 5323) and range (df-rn 5322). For an alternate definition, see dfima2 5678. (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 5314 . 2 class (𝐴𝐵)
41, 2cres 5313 . . 3 class (𝐴𝐵)
54crn 5312 . 2 class ran (𝐴𝐵)
63, 5wceq 1637 1 wff (𝐴𝐵) = ran (𝐴𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  resima  5634  resima2  5635  imaeq1  5671  imaeq2  5672  dfima2  5678  nfima  5684  rnresi  5689  resiima  5690  ima0  5691  imadisj  5694  imass1  5710  imass2  5711  imaundi  5756  imaundir  5757  inimass  5760  rninxp  5784  imainrect  5786  xpima  5787  dfrn4  5806  imacnvcnv  5810  imadmres  5841  mptpreima  5842  rnco2  5856  funcnvres  6174  funimacnv  6177  fnima  6217  fores  6336  f1ores  6363  f1orescnv  6364  foimacnv  6366  resdif  6369  fvrnressn  6648  funfvima  6713  funiunfv  6726  soisores  6797  resfunexgALT  7355  curry1  7499  curry2  7502  fparlem3  7509  fparlem4  7510  smores2  7683  tz7.44-3  7736  tz7.49c  7773  seqomlem2  7778  seqomlem3  7779  seqomlem4  7780  sbthlem4  8308  sbthlem6  8310  sbthlem8  8312  fodomfi  8474  dffi3  8572  marypha1lem  8574  marypha2lem4  8579  ordtypelem3  8660  ordtypelem9  8666  wdomima2g  8726  rankwflemb  8899  dfac8alem  9131  dfac12lem1  9246  zorn2lem1  9599  ttukeylem3  9614  imadomg  9637  iunfo  9642  fpwwe2lem6  9738  fpwwe2lem9  9741  fpwwe2lem13  9745  gruima  9905  peano5nni  11304  1nn  11312  peano2nn  11313  seqval  13031  hashimarn  13440  hashf1lem1  13452  frmdss2  17601  ghmima  17879  conjsubg  17890  gsumzaddlem  18518  gsumxp  18572  dprd2da  18639  dmdprdsplit2lem  18642  ablfac1b  18667  mplsubrglem  19644  pjdm  20257  lindsmm  20373  tgrest  21173  cnconst2  21297  imacmp  21410  cmpfi  21421  connima  21438  kgencn3  21571  ptpjopn  21625  xkoccn  21632  txkgen  21665  qtoprest  21730  hmeores  21784  txflf  22019  subgntr  22119  opnsubg  22120  clsnsg  22122  tgpconncomp  22125  snclseqg  22128  tsmsf1o  22157  tsmsxplem1  22165  fmucndlem  22304  ovolicc2lem4  23497  mbflimsup  23643  itg1addlem4  23676  ellimc2  23851  c1lip3  23972  lhop  23989  dvcnvrelem1  23990  mdegfval  24032  aalioulem3  24299  taylthlem2  24338  efifo  24504  dfrelog  24522  efopnlem2  24613  xrlimcnp  24905  fsumdvdsmul  25131  dchrghm  25191  uhgrspan1  26407  upgrreslem  26408  umgrreslem  26409  ex-ima  27626  imadifxp  29735  fresf1o  29756  elimampt  29761  imafi2  29812  ffsrn  29827  mbfmcst  30642  0rrv  30834  cvmliftmolem1  31581  cvmlift2lem9a  31603  cvmlift2lem9  31611  mrsubff1o  31730  msubff1o  31772  rdgprc  32015  dfrdg2  32016  madeval  32251  dfon4  32316  ivthALT  32646  mptsnunlem  33497  dissneqlem  33499  icoreelrnab  33513  icoreunrn  33518  poimirlem3  33720  poimirlem9  33726  poimirlem16  33733  poimirlem19  33736  poimirlem30  33747  cnres2  33868  rnresequniqs  34412  diaintclN  36833  dibintclN  36942  dihintcl  37119  imaiinfv  37752  diophrw  37818  dnnumch1  38109  fnwe2lem2  38116  hbtlem6  38194  imanonrel  38393  rp-imass  38559  csbima12gALTVD  39621  mptima  39915  imassmpt  39958  limsupvaluz  40414  funcoressn  41655
  Copyright terms: Public domain W3C validator