Definition df-ima 5627

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 30412). Contrast with restriction (df-res 5626) and range (df-rn 5625). For an alternate definition, see dfima2 6008. (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 5617	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5616	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5615	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1541	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  5961  resima2  5962  elimampt  5989  imaeq1  6001  imaeq2  6002  dfima2  6008  nfima  6014  mptima  6018  rnresi  6021  resiima  6022  ima0  6023  imadisj  6026  imass1  6047  imass2  6048  imaundi  6093  imaundir  6094  imadifssran  6095  inimass  6099  rninxp  6123  imainrect  6125  xpima  6126  dfrn4  6146  imacnvcnv  6150  imadmres  6178  mptpreima  6182  rnco2  6197  resssxp  6213  funcnvres  6555  funimacnv  6558  f1imadifssran  6563  fnima  6607  fores  6741  f1ores  6773  f1orescnv  6774  foimacnv  6776  resdif  6780  rescnvimafod  7001  fvrnressn  7089  funfvima  7159  funiunfv  7177  soisores  7256  elimampo  7478  resfunexgALT  7875  curry1  8029  curry2  8032  fparlem3  8039  fparlem4  8040  fsplitfpar  8043  smores2  8269  tz7.44-3  8322  tz7.49c  8360  seqomlem2  8365  seqomlem3  8366  seqomlem4  8367  sbthlem4  8998  sbthlem6  9000  sbthlem8  9002  fodomfi  9191  pwfir  9196  fodomfiOLD  9209  dffi3  9310  marypha1lem  9312  marypha2lem4  9317  ordtypelem3  9401  ordtypelem9  9407  wdomima2g  9467  rankwflemb  9678  dfac8alem  9912  dfac12lem1  10027  zorn2lem1  10379  ttukeylem3  10394  imadomg  10417  iunfo  10422  fpwwe2lem5  10518  fpwwe2lem8  10521  fpwwe2lem12  10525  gruima  10685  peano5nni  12120  1nn  12128  peano2nn  12129  seqval  13911  hashimarn  14339  hashf1lem1  14354  frmdss2  18763  ghmima  19142  conjsubg  19155  gsumzaddlem  19826  gsumxp  19881  dprd2da  19949  dmdprdsplit2lem  19952  ablfac1b  19977  imadrhmcl  20705  pjdm  21637  lindsmm  21758  mplsubrglem  21934  tgrest  23067  cnconst2  23191  imacmp  23305  cmpfi  23316  connima  23333  kgencn3  23466  ptpjopn  23520  xkoccn  23527  txkgen  23560  qtoprest  23625  hmeores  23679  txflf  23914  subgntr  24015  opnsubg  24016  clsnsg  24018  tgpconncomp  24021  snclseqg  24024  tsmsf1o  24053  tsmsxplem1  24061  fmucndlem  24198  ovolicc2lem4  25441  mbflimsup  25587  itg1addlem4  25620  ellimc2  25798  c1lip3  25924  lhop  25941  dvcnvrelem1  25942  mdegfval  25987  aalioulem3  26262  taylthlem2  26302  taylthlem2OLD  26303  efifo  26476  dfrelog  26494  efopnlem2  26586  xrlimcnp  26898  fsumdvdsmul  27125  fsumdvdsmulOLD  27127  dchrghm  27187  madeval  27786  seqsval  28211  noseq0  28213  noseqp1  28214  noseqind  28215  om2noseqfo  28221  dfnns2  28290  uhgrspan1  29274  upgrreslem  29275  umgrreslem  29276  ex-ima  30412  imadifxp  32571  fresf1o  32603  imafi2  32683  ffsrn  32701  pfxrn3  32912  gsumzresunsn  33026  gsumhashmul  33031  cycpmconjvlem  33100  tocyccntz  33103  qusima  33363  lmimdim  33606  dimkerim  33630  mbfmcst  34262  0rrv  34454  onvf1odlem3  35117  cvmliftmolem1  35293  cvmlift2lem9a  35315  cvmlift2lem9  35323  mrsubff1o  35527  msubff1o  35569  rdgprc  35807  dfrdg2  35808  dfon4  35906  ivthALT  36348  mptsnunlem  37351  dissneqlem  37353  icoreelrnab  37367  icoreunrn  37372  poimirlem3  37642  poimirlem9  37648  poimirlem16  37655  poimirlem19  37658  poimirlem30  37669  cnres2  37782  rnresequniqs  38341  diaintclN  41076  dibintclN  41185  dihintcl  41362  imadomfi  42014  aks6d1c2  42142  aks6d1c6lem3  42184  imaopab  42243  imaiinfv  42705  diophrw  42771  dnnumch1  43056  fnwe2lem2  43063  hbtlem6  43141  imanonrel  43605  csbima12gALTVD  44908  orbitinit  44968  orbitcl  44969  imassmpt  45278  limsupvaluz  45725  funcoressn  47052  fcoreslem2  47074