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 5097
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 27187). Contrast with restriction (df-res 5096) and range (df-rn 5095). For an alternate definition, see dfima2 5437. (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 5087 . 2 class (𝐴𝐵)
41, 2cres 5086 . . 3 class (𝐴𝐵)
54crn 5085 . 2 class ran (𝐴𝐵)
63, 5wceq 1480 1 wff (𝐴𝐵) = ran (𝐴𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  resima  5400  resima2  5401  resima2OLD  5402  imaeq1  5430  imaeq2  5431  dfima2  5437  nfima  5443  rnresi  5448  resiima  5449  ima0  5450  imadisj  5453  imass1  5469  imass2  5470  imaundi  5514  imaundir  5515  inimass  5518  rninxp  5542  imainrect  5544  xpima  5545  dfrn4  5564  imacnvcnv  5568  imadmres  5596  mptpreima  5597  rnco2  5611  funcnvres  5935  funimacnv  5938  fnima  5977  fores  6091  f1ores  6118  f1orescnv  6119  foimacnv  6121  resdif  6124  fvrnressn  6393  funfvima  6457  funiunfv  6471  soisores  6542  resfunexgALT  7091  curry1  7229  curry2  7232  fparlem3  7239  fparlem4  7240  smores2  7411  tz7.44-3  7464  tz7.49c  7501  seqomlem2  7506  seqomlem3  7507  seqomlem4  7508  sbthlem4  8033  sbthlem6  8035  sbthlem8  8037  fodomfi  8199  dffi3  8297  marypha1lem  8299  marypha2lem4  8304  ordtypelem3  8385  ordtypelem9  8391  wdomima2g  8451  rankwflemb  8616  dfac8alem  8812  dfac12lem1  8925  zorn2lem1  9278  ttukeylem3  9293  imadomg  9316  iunfo  9321  fpwwe2lem6  9417  fpwwe2lem9  9420  fpwwe2lem13  9424  gruima  9584  peano5nni  10983  1nn  10991  peano2nn  10992  seqval  12768  hashimarn  13181  hashf1lem1  13193  frmdss2  17340  ghmima  17621  conjsubg  17632  gsumzaddlem  18261  gsumxp  18315  dprd2da  18381  dmdprdsplit2lem  18384  ablfac1b  18409  mplsubrglem  19379  pjdm  19991  lindsmm  20107  tgrest  20903  cnconst2  21027  imacmp  21140  cmpfi  21151  connima  21168  kgencn3  21301  ptpjopn  21355  xkoccn  21362  txkgen  21395  qtoprest  21460  hmeores  21514  txflf  21750  subgntr  21850  opnsubg  21851  clsnsg  21853  tgpconncomp  21856  snclseqg  21859  tsmsf1o  21888  tsmsxplem1  21896  fmucndlem  22035  ovolicc2lem4  23228  mbflimsup  23373  itg1addlem4  23406  ellimc2  23581  c1lip3  23700  lhop  23717  dvcnvrelem1  23718  mdegfval  23760  aalioulem3  24027  taylthlem2  24066  efifo  24231  dfrelog  24250  efopnlem2  24337  xrlimcnp  24629  fsumdvdsmul  24855  dchrghm  24915  uhgrspan1  26122  ex-ima  27187  imadifxp  29300  fresf1o  29318  imafi2  29373  ffsrn  29388  mbfmcst  30144  0rrv  30336  cvmliftmolem1  31024  cvmlift2lem9a  31046  cvmlift2lem9  31054  mrsubff1o  31173  msubff1o  31215  rdgprc  31454  dfrdg2  31455  dfon4  31695  ivthALT  32025  mptsnunlem  32856  dissneqlem  32858  icoreelrnab  32873  icoreunrn  32878  poimirlem3  33083  poimirlem9  33089  poimirlem16  33096  poimirlem19  33099  poimirlem30  33110  cnres2  33233  diaintclN  35866  dibintclN  35975  dihintcl  36152  imaiinfv  36775  diophrw  36841  dnnumch1  37133  fnwe2lem2  37140  hbtlem6  37219  imanonrel  37419  rp-imass  37586  csbima12gALTOLD  38579  csbima12gALTVD  38655  mptima  38947  limsupvaluz  39376  funcoressn  40541
  Copyright terms: Public domain W3C validator