Definition df-ima 5651

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 29449). Contrast with restriction (df-res 5650) and range (df-rn 5649). For an alternate definition, see dfima2 6020. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
df-ima	⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

Detailed syntax breakdown of Definition df-ima

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	cima 5641	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5640	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5639	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1541	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  5976  resima2  5977  imaeq1  6013  imaeq2  6014  dfima2  6020  nfima  6026  mptima  6030  rnresi  6032  resiima  6033  ima0  6034  imadisj  6037  imass1  6058  imass2  6059  imaundi  6107  imaundir  6108  inimass  6112  rninxp  6136  imainrect  6138  xpima  6139  dfrn4  6159  imacnvcnv  6163  imadmres  6191  mptpreima  6195  rnco2  6210  resssxp  6227  funcnvres  6584  funimacnv  6587  fnima  6636  fores  6771  f1ores  6803  f1orescnv  6804  foimacnv  6806  resdif  6810  rescnvimafod  7029  fvrnressn  7112  funfvima  7185  funiunfv  7200  soisores  7277  resfunexgALT  7885  curry1  8041  curry2  8044  fparlem3  8051  fparlem4  8052  fsplitfpar  8055  smores2  8305  tz7.44-3  8359  tz7.49c  8397  seqomlem2  8402  seqomlem3  8403  seqomlem4  8404  sbthlem4  9037  sbthlem6  9039  sbthlem8  9041  pwfir  9127  fodomfi  9276  dffi3  9376  marypha1lem  9378  marypha2lem4  9383  ordtypelem3  9465  ordtypelem9  9471  wdomima2g  9531  rankwflemb  9738  dfac8alem  9974  dfac12lem1  10088  zorn2lem1  10441  ttukeylem3  10456  imadomg  10479  iunfo  10484  fpwwe2lem5  10580  fpwwe2lem8  10583  fpwwe2lem12  10587  gruima  10747  peano5nni  12165  1nn  12173  peano2nn  12174  seqval  13927  hashimarn  14350  hashf1lem1  14365  hashf1lem1OLD  14366  frmdss2  18687  ghmima  19043  conjsubg  19054  gsumzaddlem  19712  gsumxp  19767  dprd2da  19835  dmdprdsplit2lem  19838  ablfac1b  19863  rnrhmsubrg  20304  imadrhmcl  20320  pjdm  21150  lindsmm  21271  mplsubrglem  21447  tgrest  22547  cnconst2  22671  imacmp  22785  cmpfi  22796  connima  22813  kgencn3  22946  ptpjopn  23000  xkoccn  23007  txkgen  23040  qtoprest  23105  hmeores  23159  txflf  23394  subgntr  23495  opnsubg  23496  clsnsg  23498  tgpconncomp  23501  snclseqg  23504  tsmsf1o  23533  tsmsxplem1  23541  fmucndlem  23680  ovolicc2lem4  24921  mbflimsup  25067  itg1addlem4  25100  itg1addlem4OLD  25101  ellimc2  25278  c1lip3  25400  lhop  25417  dvcnvrelem1  25418  mdegfval  25464  aalioulem3  25731  taylthlem2  25770  efifo  25940  dfrelog  25958  efopnlem2  26049  xrlimcnp  26355  fsumdvdsmul  26581  dchrghm  26641  madeval  27225  uhgrspan1  28314  upgrreslem  28315  umgrreslem  28316  ex-ima  29449  imadifxp  31586  fresf1o  31612  elimampt  31619  imafi2  31696  ffsrn  31714  pfxrn3  31867  gsumzresunsn  31966  gsumhashmul  31968  cycpmconjvlem  32060  tocyccntz  32063  qusima  32261  lmimdim  32387  dimkerim  32409  mbfmcst  32948  0rrv  33140  cvmliftmolem1  33962  cvmlift2lem9a  33984  cvmlift2lem9  33992  mrsubff1o  34196  msubff1o  34238  rdgprc  34455  dfrdg2  34456  dfon4  34554  ivthALT  34883  mptsnunlem  35882  dissneqlem  35884  icoreelrnab  35898  icoreunrn  35903  poimirlem3  36154  poimirlem9  36160  poimirlem16  36167  poimirlem19  36170  poimirlem30  36181  cnres2  36295  rnresequniqs  36866  diaintclN  39594  dibintclN  39703  dihintcl  39880  imaopab  40727  imaiinfv  41074  diophrw  41140  dnnumch1  41429  fnwe2lem2  41436  hbtlem6  41514  imanonrel  41987  csbima12gALTVD  43301  imassmpt  43612  limsupvaluz  44069  funcoressn  45396  fcoreslem2  45418