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 5562
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 28149). Contrast with restriction (df-res 5561) and range (df-rn 5560). For an alternate definition, see dfima2 5925. (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 5552 . 2 class (𝐴𝐵)
41, 2cres 5551 . . 3 class (𝐴𝐵)
54crn 5550 . 2 class ran (𝐴𝐵)
63, 5wceq 1528 1 wff (𝐴𝐵) = ran (𝐴𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  resima  5881  resima2  5882  imaeq1  5918  imaeq2  5919  dfima2  5925  nfima  5931  mptima  5935  rnresi  5937  resiima  5938  ima0  5939  imadisj  5942  imass1  5958  imass2  5959  imaundi  6002  imaundir  6003  inimass  6006  rninxp  6030  imainrect  6032  xpima  6033  dfrn4  6053  imacnvcnv  6057  imadmres  6085  mptpreima  6086  rnco2  6100  funcnvres  6426  funimacnv  6429  fnima  6472  fores  6594  f1ores  6623  f1orescnv  6624  foimacnv  6626  resdif  6629  fvrnressn  6916  funfvima  6984  funiunfv  6998  soisores  7069  resfunexgALT  7640  curry1  7790  curry2  7793  fparlem3  7800  fparlem4  7801  fsplitfpar  7805  smores2  7982  tz7.44-3  8035  tz7.49c  8073  seqomlem2  8078  seqomlem3  8079  seqomlem4  8080  sbthlem4  8619  sbthlem6  8621  sbthlem8  8623  fodomfi  8786  dffi3  8884  marypha1lem  8886  marypha2lem4  8891  ordtypelem3  8973  ordtypelem9  8979  wdomima2g  9039  rankwflemb  9211  dfac8alem  9444  dfac12lem1  9558  zorn2lem1  9907  ttukeylem3  9922  imadomg  9945  iunfo  9950  fpwwe2lem6  10046  fpwwe2lem9  10049  fpwwe2lem13  10053  gruima  10213  peano5nni  11630  1nn  11638  peano2nn  11639  seqval  13370  hashimarn  13791  hashf1lem1  13803  frmdss2  18018  ghmima  18319  conjsubg  18330  gsumzaddlem  18972  gsumxp  19027  dprd2da  19095  dmdprdsplit2lem  19098  ablfac1b  19123  rnrhmsubrg  19498  mplsubrglem  20149  pjdm  20781  lindsmm  20902  tgrest  21697  cnconst2  21821  imacmp  21935  cmpfi  21946  connima  21963  kgencn3  22096  ptpjopn  22150  xkoccn  22157  txkgen  22190  qtoprest  22255  hmeores  22309  txflf  22544  subgntr  22644  opnsubg  22645  clsnsg  22647  tgpconncomp  22650  snclseqg  22653  tsmsf1o  22682  tsmsxplem1  22690  fmucndlem  22829  ovolicc2lem4  24050  mbflimsup  24196  itg1addlem4  24229  ellimc2  24404  c1lip3  24525  lhop  24542  dvcnvrelem1  24543  mdegfval  24585  aalioulem3  24852  taylthlem2  24891  efifo  25058  dfrelog  25076  efopnlem2  25167  xrlimcnp  25474  fsumdvdsmul  25700  dchrghm  25760  uhgrspan1  27013  upgrreslem  27014  umgrreslem  27015  ex-ima  28149  imadifxp  30280  fresf1o  30305  elimampt  30312  imafi2  30374  ffsrn  30392  pfxrn3  30545  gsumzresunsn  30619  cycpmconjvlem  30711  tocyccntz  30714  dimkerim  30923  mbfmcst  31417  0rrv  31609  cvmliftmolem1  32426  cvmlift2lem9a  32448  cvmlift2lem9  32456  mrsubff1o  32660  msubff1o  32702  rdgprc  32937  dfrdg2  32938  madeval  33187  dfon4  33252  ivthALT  33581  mptsnunlem  34502  dissneqlem  34504  icoreelrnab  34518  icoreunrn  34523  poimirlem3  34777  poimirlem9  34783  poimirlem16  34790  poimirlem19  34793  poimirlem30  34804  cnres2  34924  rnresequniqs  35472  diaintclN  38076  dibintclN  38185  dihintcl  38362  imaopab  38999  imaiinfv  39170  diophrw  39236  dnnumch1  39524  fnwe2lem2  39531  hbtlem6  39609  imanonrel  39833  rp-imass  39997  csbima12gALTVD  41111  imassmpt  41417  limsupvaluz  41869  funcoressn  43158
  Copyright terms: Public domain W3C validator