Definition df-ima 5658

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 30588). Contrast with restriction (df-res 5657) and range (df-rn 5656). For an alternate definition, see dfima2 6046. (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 5648	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5647	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5646	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1559	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  5999  resima2  6000  elimampt  6027  imaeq1  6039  imaeq2  6040  dfima2  6046  nfima  6052  mptima  6056  rnresi  6059  resiima  6060  ima0  6061  imadisj  6064  imass1  6085  imass2  6086  imaundi  6129  imaundir  6130  imadifssran  6131  inimass  6135  rninxp  6159  imainrect  6161  xpima  6162  dfrn4  6183  imacnvcnv  6187  imadmres  6215  mptpreima  6219  rnco2  6235  resssxp  6251  funcnvres  6593  funimacnv  6596  f1imadifssran  6601  fnima  6645  fores  6782  f1ores  6815  f1orescnv  6816  foimacnv  6818  resdif  6822  rescnvimafod  7048  fvrnressn  7138  funfvima  7208  funiunfv  7226  soisores  7305  elimampo  7527  resfunexgALT  7923  curry1  8076  curry2  8079  fparlem3  8086  fparlem4  8087  fsplitfpar  8090  smores2  8318  tz7.44-3  8372  tz7.49c  8410  seqomlem2  8415  seqomlem3  8416  seqomlem4  8417  sbthlem4  9056  sbthlem6  9058  sbthlem8  9060  fodomfi  9250  pwfir  9255  fodomfiOLD  9268  imafi2  9299  dffi3  9372  marypha1lem  9374  marypha2lem4  9379  ordtypelem3  9463  ordtypelem9  9469  wdomima2g  9529  rankwflemb  9746  dfac8alem  9980  dfac12lem1  10095  zorn2lem1  10448  ttukeylem3  10463  imadomg  10486  iunfo  10491  fpwwe2lem5  10588  fpwwe2lem8  10591  fpwwe2lem12  10595  gruima  10755  peano5nni  12208  1nn  12216  peano2nn  12217  seqval  14020  hashimarn  14448  hashf1lem1  14463  frmdss2  18878  ghmima  19258  conjsubg  19271  gsumzaddlem  19942  gsumxp  19997  dprd2da  20065  dmdprdsplit2lem  20068  ablfac1b  20093  imadrhmcl  20824  pjdm  21737  lindsmm  21858  mplsubrglem  22033  tgrest  23197  cnconst2  23321  imacmp  23435  cmpfi  23446  connima  23463  kgencn3  23596  ptpjopn  23650  xkoccn  23657  txkgen  23690  qtoprest  23755  hmeores  23809  txflf  24044  subgntr  24145  opnsubg  24146  clsnsg  24148  tgpconncomp  24151  snclseqg  24154  tsmsf1o  24183  tsmsxplem1  24191  fmucndlem  24328  ovolicc2lem4  25560  mbflimsup  25706  itg1addlem4  25739  ellimc2  25917  c1lip3  26039  lhop  26056  dvcnvrelem1  26057  mdegfval  26100  aalioulem3  26373  taylthlem2  26412  efifo  26587  dfrelog  26605  efopnlem2  26697  xrlimcnp  27008  fsumdvdsmul  27234  dchrghm  27295  madeval  27900  seqsval  28356  noseq0  28358  noseqp1  28359  noseqind  28360  om2noseqfo  28366  dfnns2  28440  uhgrspan1  29448  upgrreslem  29449  umgrreslem  29450  ex-ima  30588  imadifxp  32748  fresf1o  32781  ffsrn  32878  pfxrn3  33078  gsumzresunsn  33201  gsumhashmul  33206  cycpmconjvlem  33280  tocyccntz  33283  qusima  33553  lmimdim  33860  dimkerim  33883  mbfmcst  34515  0rrv  34707  onvf1odlem3  35408  cvmliftmolem1  35584  cvmlift2lem9a  35606  cvmlift2lem9  35614  mrsubff1o  35818  msubff1o  35860  rdgprc  36095  dfrdg2  36096  dfon4  36194  ivthALT  36648  mptsnunlem  37785  dissneqlem  37787  icoreelrnab  37801  icoreunrn  37806  poimirlem3  38075  poimirlem9  38081  poimirlem16  38088  poimirlem19  38091  poimirlem30  38102  cnres2  38215  rnresequniqs  38786  diaintclN  41635  dibintclN  41744  dihintcl  41921  imadomfi  42572  aks6d1c2  42700  aks6d1c6lem3  42742  imaopab  42803  imaiinfv  43227  diophrw  43293  dnnumch1  43574  fnwe2lem2  43581  hbtlem6  43659  imanonrel  44122  csbima12gALTVD  45425  orbitinit  45485  orbitcl  45486  imassmpt  45790  limsupvaluz  46235  funcoressn  47589  fcoreslem2  47611