Definition df-ima 5635

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

This definition is referenced by:  resima  5972  resima2  5973  elimampt  6000  imaeq1  6012  imaeq2  6013  dfima2  6019  nfima  6025  mptima  6029  rnresi  6032  resiima  6033  ima0  6034  imadisj  6037  imass1  6058  imass2  6059  imaundi  6105  imaundir  6106  imadifssran  6107  inimass  6111  rninxp  6135  imainrect  6137  xpima  6138  dfrn4  6158  imacnvcnv  6162  imadmres  6190  mptpreima  6194  rnco2  6210  resssxp  6226  funcnvres  6568  funimacnv  6571  f1imadifssran  6576  fnima  6620  fores  6754  f1ores  6786  f1orescnv  6787  foimacnv  6789  resdif  6793  rescnvimafod  7017  fvrnressn  7106  funfvima  7176  funiunfv  7194  soisores  7273  elimampo  7495  resfunexgALT  7892  curry1  8045  curry2  8048  fparlem3  8055  fparlem4  8056  fsplitfpar  8059  smores2  8285  tz7.44-3  8338  tz7.49c  8376  seqomlem2  8381  seqomlem3  8382  seqomlem4  8383  sbthlem4  9019  sbthlem6  9021  sbthlem8  9023  fodomfi  9213  pwfir  9218  fodomfiOLD  9231  imafi2  9262  dffi3  9335  marypha1lem  9337  marypha2lem4  9342  ordtypelem3  9426  ordtypelem9  9432  wdomima2g  9492  rankwflemb  9706  dfac8alem  9940  dfac12lem1  10055  zorn2lem1  10407  ttukeylem3  10422  imadomg  10445  iunfo  10450  fpwwe2lem5  10547  fpwwe2lem8  10550  fpwwe2lem12  10554  gruima  10714  peano5nni  12166  1nn  12174  peano2nn  12175  seqval  13963  hashimarn  14391  hashf1lem1  14406  frmdss2  18820  ghmima  19201  conjsubg  19214  gsumzaddlem  19885  gsumxp  19940  dprd2da  20008  dmdprdsplit2lem  20011  ablfac1b  20036  imadrhmcl  20763  pjdm  21695  lindsmm  21816  mplsubrglem  21991  tgrest  23133  cnconst2  23257  imacmp  23371  cmpfi  23382  connima  23399  kgencn3  23532  ptpjopn  23586  xkoccn  23593  txkgen  23626  qtoprest  23691  hmeores  23745  txflf  23980  subgntr  24081  opnsubg  24082  clsnsg  24084  tgpconncomp  24087  snclseqg  24090  tsmsf1o  24119  tsmsxplem1  24127  fmucndlem  24264  ovolicc2lem4  25496  mbflimsup  25642  itg1addlem4  25675  ellimc2  25853  c1lip3  25976  lhop  25993  dvcnvrelem1  25994  mdegfval  26039  aalioulem3  26313  taylthlem2  26353  taylthlem2OLD  26354  efifo  26527  dfrelog  26545  efopnlem2  26637  xrlimcnp  26949  fsumdvdsmul  27176  fsumdvdsmulOLD  27178  dchrghm  27238  madeval  27843  seqsval  28299  noseq0  28301  noseqp1  28302  noseqind  28303  om2noseqfo  28309  dfnns2  28383  uhgrspan1  29391  upgrreslem  29392  umgrreslem  29393  ex-ima  30532  imadifxp  32691  fresf1o  32724  ffsrn  32821  pfxrn3  33021  gsumzresunsn  33143  gsumhashmul  33148  cycpmconjvlem  33222  tocyccntz  33225  qusima  33488  lmimdim  33768  dimkerim  33792  mbfmcst  34424  0rrv  34616  onvf1odlem3  35308  cvmliftmolem1  35484  cvmlift2lem9a  35506  cvmlift2lem9  35514  mrsubff1o  35718  msubff1o  35760  rdgprc  35995  dfrdg2  35996  dfon4  36094  ivthALT  36538  mptsnunlem  37665  dissneqlem  37667  icoreelrnab  37681  icoreunrn  37686  poimirlem3  37955  poimirlem9  37961  poimirlem16  37968  poimirlem19  37971  poimirlem30  37982  cnres2  38095  rnresequniqs  38666  diaintclN  41515  dibintclN  41624  dihintcl  41801  imadomfi  42452  aks6d1c2  42580  aks6d1c6lem3  42622  imaopab  42683  imaiinfv  43136  diophrw  43202  dnnumch1  43487  fnwe2lem2  43494  hbtlem6  43572  imanonrel  44035  csbima12gALTVD  45338  orbitinit  45398  orbitcl  45399  imassmpt  45706  limsupvaluz  46151  funcoressn  47487  fcoreslem2  47509