Definition df-ima 5638

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 30537). Contrast with restriction (df-res 5637) and range (df-rn 5636). For an alternate definition, see dfima2 6021. (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 5628	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5627	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5626	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1547	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  5974  resima2  5975  elimampt  6002  imaeq1  6014  imaeq2  6015  dfima2  6021  nfima  6027  mptima  6031  rnresi  6034  resiima  6035  ima0  6036  imadisj  6039  imass1  6060  imass2  6061  imaundi  6107  imaundir  6108  imadifssran  6109  inimass  6113  rninxp  6137  imainrect  6139  xpima  6140  dfrn4  6160  imacnvcnv  6164  imadmres  6192  mptpreima  6196  rnco2  6212  resssxp  6228  funcnvres  6570  funimacnv  6573  f1imadifssran  6578  fnima  6622  fores  6756  f1ores  6788  f1orescnv  6789  foimacnv  6791  resdif  6795  rescnvimafod  7021  fvrnressn  7111  funfvima  7181  funiunfv  7199  soisores  7278  elimampo  7500  resfunexgALT  7897  curry1  8050  curry2  8053  fparlem3  8060  fparlem4  8061  fsplitfpar  8064  smores2  8291  tz7.44-3  8344  tz7.49c  8382  seqomlem2  8387  seqomlem3  8388  seqomlem4  8389  sbthlem4  9025  sbthlem6  9027  sbthlem8  9029  fodomfi  9219  pwfir  9224  fodomfiOLD  9237  imafi2  9268  dffi3  9341  marypha1lem  9343  marypha2lem4  9348  ordtypelem3  9432  ordtypelem9  9438  wdomima2g  9498  rankwflemb  9715  dfac8alem  9949  dfac12lem1  10064  zorn2lem1  10416  ttukeylem3  10431  imadomg  10454  iunfo  10459  fpwwe2lem5  10556  fpwwe2lem8  10559  fpwwe2lem12  10563  gruima  10723  peano5nni  12175  1nn  12183  peano2nn  12184  seqval  13972  hashimarn  14400  hashf1lem1  14415  frmdss2  18829  ghmima  19210  conjsubg  19223  gsumzaddlem  19894  gsumxp  19949  dprd2da  20017  dmdprdsplit2lem  20020  ablfac1b  20045  imadrhmcl  20776  pjdm  21689  lindsmm  21810  mplsubrglem  21985  tgrest  23149  cnconst2  23273  imacmp  23387  cmpfi  23398  connima  23415  kgencn3  23548  ptpjopn  23602  xkoccn  23609  txkgen  23642  qtoprest  23707  hmeores  23761  txflf  23996  subgntr  24097  opnsubg  24098  clsnsg  24100  tgpconncomp  24103  snclseqg  24106  tsmsf1o  24135  tsmsxplem1  24143  fmucndlem  24280  ovolicc2lem4  25512  mbflimsup  25658  itg1addlem4  25691  ellimc2  25869  c1lip3  25991  lhop  26008  dvcnvrelem1  26009  mdegfval  26052  aalioulem3  26325  taylthlem2  26364  efifo  26536  dfrelog  26554  efopnlem2  26646  xrlimcnp  26957  fsumdvdsmul  27183  dchrghm  27244  madeval  27849  seqsval  28305  noseq0  28307  noseqp1  28308  noseqind  28309  om2noseqfo  28315  dfnns2  28389  uhgrspan1  29397  upgrreslem  29398  umgrreslem  29399  ex-ima  30537  imadifxp  32697  fresf1o  32730  ffsrn  32827  pfxrn3  33027  gsumzresunsn  33150  gsumhashmul  33155  cycpmconjvlem  33229  tocyccntz  33232  qusima  33498  lmimdim  33795  dimkerim  33818  mbfmcst  34450  0rrv  34642  onvf1odlem3  35334  cvmliftmolem1  35510  cvmlift2lem9a  35532  cvmlift2lem9  35540  mrsubff1o  35744  msubff1o  35786  rdgprc  36021  dfrdg2  36022  dfon4  36120  ivthALT  36564  mptsnunlem  37701  dissneqlem  37703  icoreelrnab  37717  icoreunrn  37722  poimirlem3  37991  poimirlem9  37997  poimirlem16  38004  poimirlem19  38007  poimirlem30  38018  cnres2  38131  rnresequniqs  38702  diaintclN  41551  dibintclN  41660  dihintcl  41837  imadomfi  42488  aks6d1c2  42616  aks6d1c6lem3  42658  imaopab  42719  imaiinfv  43143  diophrw  43209  dnnumch1  43490  fnwe2lem2  43497  hbtlem6  43575  imanonrel  44038  csbima12gALTVD  45341  orbitinit  45401  orbitcl  45402  imassmpt  45707  limsupvaluz  46152  funcoressn  47506  fcoreslem2  47528