Definition df-ima 5634

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 30433). Contrast with restriction (df-res 5633) and range (df-rn 5632). For an alternate definition, see dfima2 6018. (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 5624	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5623	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5622	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1541	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  5971  resima2  5972  elimampt  5999  imaeq1  6011  imaeq2  6012  dfima2  6018  nfima  6024  mptima  6028  rnresi  6031  resiima  6032  ima0  6033  imadisj  6036  imass1  6057  imass2  6058  imaundi  6104  imaundir  6105  imadifssran  6106  inimass  6110  rninxp  6134  imainrect  6136  xpima  6137  dfrn4  6157  imacnvcnv  6161  imadmres  6189  mptpreima  6193  rnco2  6209  resssxp  6225  funcnvres  6567  funimacnv  6570  f1imadifssran  6575  fnima  6619  fores  6753  f1ores  6785  f1orescnv  6786  foimacnv  6788  resdif  6792  rescnvimafod  7015  fvrnressn  7103  funfvima  7173  funiunfv  7191  soisores  7270  elimampo  7492  resfunexgALT  7889  curry1  8043  curry2  8046  fparlem3  8053  fparlem4  8054  fsplitfpar  8057  smores2  8283  tz7.44-3  8336  tz7.49c  8374  seqomlem2  8379  seqomlem3  8380  seqomlem4  8381  sbthlem4  9013  sbthlem6  9015  sbthlem8  9017  fodomfi  9206  pwfir  9211  fodomfiOLD  9224  dffi3  9325  marypha1lem  9327  marypha2lem4  9332  ordtypelem3  9416  ordtypelem9  9422  wdomima2g  9482  rankwflemb  9696  dfac8alem  9930  dfac12lem1  10045  zorn2lem1  10397  ttukeylem3  10412  imadomg  10435  iunfo  10440  fpwwe2lem5  10536  fpwwe2lem8  10539  fpwwe2lem12  10543  gruima  10703  peano5nni  12138  1nn  12146  peano2nn  12147  seqval  13929  hashimarn  14357  hashf1lem1  14372  frmdss2  18781  ghmima  19159  conjsubg  19172  gsumzaddlem  19843  gsumxp  19898  dprd2da  19966  dmdprdsplit2lem  19969  ablfac1b  19994  imadrhmcl  20722  pjdm  21654  lindsmm  21775  mplsubrglem  21951  tgrest  23084  cnconst2  23208  imacmp  23322  cmpfi  23333  connima  23350  kgencn3  23483  ptpjopn  23537  xkoccn  23544  txkgen  23577  qtoprest  23642  hmeores  23696  txflf  23931  subgntr  24032  opnsubg  24033  clsnsg  24035  tgpconncomp  24038  snclseqg  24041  tsmsf1o  24070  tsmsxplem1  24078  fmucndlem  24215  ovolicc2lem4  25458  mbflimsup  25604  itg1addlem4  25637  ellimc2  25815  c1lip3  25941  lhop  25958  dvcnvrelem1  25959  mdegfval  26004  aalioulem3  26279  taylthlem2  26319  taylthlem2OLD  26320  efifo  26493  dfrelog  26511  efopnlem2  26603  xrlimcnp  26915  fsumdvdsmul  27142  fsumdvdsmulOLD  27144  dchrghm  27204  madeval  27803  seqsval  28228  noseq0  28230  noseqp1  28231  noseqind  28232  om2noseqfo  28238  dfnns2  28307  uhgrspan1  29292  upgrreslem  29293  umgrreslem  29294  ex-ima  30433  imadifxp  32592  fresf1o  32624  imafi2  32704  ffsrn  32722  pfxrn3  32933  gsumzresunsn  33047  gsumhashmul  33052  cycpmconjvlem  33121  tocyccntz  33124  qusima  33384  lmimdim  33627  dimkerim  33651  mbfmcst  34283  0rrv  34475  onvf1odlem3  35160  cvmliftmolem1  35336  cvmlift2lem9a  35358  cvmlift2lem9  35366  mrsubff1o  35570  msubff1o  35612  rdgprc  35847  dfrdg2  35848  dfon4  35946  ivthALT  36390  mptsnunlem  37393  dissneqlem  37395  icoreelrnab  37409  icoreunrn  37414  poimirlem3  37673  poimirlem9  37679  poimirlem16  37686  poimirlem19  37689  poimirlem30  37700  cnres2  37813  rnresequniqs  38376  diaintclN  41167  dibintclN  41276  dihintcl  41453  imadomfi  42105  aks6d1c2  42233  aks6d1c6lem3  42275  imaopab  42339  imaiinfv  42800  diophrw  42866  dnnumch1  43151  fnwe2lem2  43158  hbtlem6  43236  imanonrel  43700  csbima12gALTVD  45003  orbitinit  45063  orbitcl  45064  imassmpt  45373  limsupvaluz  45820  funcoressn  47156  fcoreslem2  47178