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 30371). Contrast with restriction (df-res 5650) and range (df-rn 5649). For an alternate definition, see dfima2 6033. (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 1540	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  5986  resima2  5987  elimampt  6014  imaeq1  6026  imaeq2  6027  dfima2  6033  nfima  6039  mptima  6043  rnresi  6046  resiima  6047  ima0  6048  imadisj  6051  imass1  6072  imass2  6073  imaundi  6122  imaundir  6123  imadifssran  6124  inimass  6128  rninxp  6152  imainrect  6154  xpima  6155  dfrn4  6175  imacnvcnv  6179  imadmres  6207  mptpreima  6211  rnco2  6226  resssxp  6243  funcnvres  6594  funimacnv  6597  f1imadifssran  6602  fnima  6648  fores  6782  f1ores  6814  f1orescnv  6815  foimacnv  6817  resdif  6821  rescnvimafod  7045  fvrnressn  7133  funfvima  7204  funiunfv  7222  soisores  7302  elimampo  7526  resfunexgALT  7926  curry1  8083  curry2  8086  fparlem3  8093  fparlem4  8094  fsplitfpar  8097  smores2  8323  tz7.44-3  8376  tz7.49c  8414  seqomlem2  8419  seqomlem3  8420  seqomlem4  8421  sbthlem4  9054  sbthlem6  9056  sbthlem8  9058  fodomfi  9261  pwfir  9266  fodomfiOLD  9281  dffi3  9382  marypha1lem  9384  marypha2lem4  9389  ordtypelem3  9473  ordtypelem9  9479  wdomima2g  9539  rankwflemb  9746  dfac8alem  9982  dfac12lem1  10097  zorn2lem1  10449  ttukeylem3  10464  imadomg  10487  iunfo  10492  fpwwe2lem5  10588  fpwwe2lem8  10591  fpwwe2lem12  10595  gruima  10755  peano5nni  12189  1nn  12197  peano2nn  12198  seqval  13977  hashimarn  14405  hashf1lem1  14420  frmdss2  18790  ghmima  19169  conjsubg  19182  gsumzaddlem  19851  gsumxp  19906  dprd2da  19974  dmdprdsplit2lem  19977  ablfac1b  20002  imadrhmcl  20706  pjdm  21616  lindsmm  21737  mplsubrglem  21913  tgrest  23046  cnconst2  23170  imacmp  23284  cmpfi  23295  connima  23312  kgencn3  23445  ptpjopn  23499  xkoccn  23506  txkgen  23539  qtoprest  23604  hmeores  23658  txflf  23893  subgntr  23994  opnsubg  23995  clsnsg  23997  tgpconncomp  24000  snclseqg  24003  tsmsf1o  24032  tsmsxplem1  24040  fmucndlem  24178  ovolicc2lem4  25421  mbflimsup  25567  itg1addlem4  25600  ellimc2  25778  c1lip3  25904  lhop  25921  dvcnvrelem1  25922  mdegfval  25967  aalioulem3  26242  taylthlem2  26282  taylthlem2OLD  26283  efifo  26456  dfrelog  26474  efopnlem2  26566  xrlimcnp  26878  fsumdvdsmul  27105  fsumdvdsmulOLD  27107  dchrghm  27167  madeval  27760  seqsval  28182  noseq0  28184  noseqp1  28185  noseqind  28186  om2noseqfo  28192  dfnns2  28261  uhgrspan1  29230  upgrreslem  29231  umgrreslem  29232  ex-ima  30371  imadifxp  32530  fresf1o  32555  imafi2  32635  ffsrn  32652  pfxrn3  32862  gsumzresunsn  32996  gsumhashmul  33001  cycpmconjvlem  33098  tocyccntz  33101  qusima  33379  lmimdim  33599  dimkerim  33623  mbfmcst  34250  0rrv  34442  onvf1odlem3  35092  cvmliftmolem1  35268  cvmlift2lem9a  35290  cvmlift2lem9  35298  mrsubff1o  35502  msubff1o  35544  rdgprc  35782  dfrdg2  35783  dfon4  35881  ivthALT  36323  mptsnunlem  37326  dissneqlem  37328  icoreelrnab  37342  icoreunrn  37347  poimirlem3  37617  poimirlem9  37623  poimirlem16  37630  poimirlem19  37633  poimirlem30  37644  cnres2  37757  rnresequniqs  38316  diaintclN  41052  dibintclN  41161  dihintcl  41338  imadomfi  41990  aks6d1c2  42118  aks6d1c6lem3  42160  imaopab  42219  imaiinfv  42681  diophrw  42747  dnnumch1  43033  fnwe2lem2  43040  hbtlem6  43118  imanonrel  43582  csbima12gALTVD  44886  orbitinit  44946  orbitcl  44947  imassmpt  45256  limsupvaluz  45706  funcoressn  47043  fcoreslem2  47065