Definition df-ima 5713

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 30474). Contrast with restriction (df-res 5712) and range (df-rn 5711). For an alternate definition, see dfima2 6091. (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 5703	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5702	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5701	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1537	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  6044  resima2  6045  elimampt  6072  imaeq1  6084  imaeq2  6085  dfima2  6091  nfima  6097  mptima  6101  rnresi  6104  resiima  6105  ima0  6106  imadisj  6109  imass1  6131  imass2  6132  imaundi  6181  imaundir  6182  inimass  6186  rninxp  6210  imainrect  6212  xpima  6213  dfrn4  6233  imacnvcnv  6237  imadmres  6265  mptpreima  6269  rnco2  6284  resssxp  6301  funcnvres  6656  funimacnv  6659  fnima  6710  fores  6844  f1ores  6876  f1orescnv  6877  foimacnv  6879  resdif  6883  rescnvimafod  7107  fvrnressn  7195  funfvima  7267  funiunfv  7285  soisores  7363  elimampo  7587  resfunexgALT  7988  curry1  8145  curry2  8148  fparlem3  8155  fparlem4  8156  fsplitfpar  8159  smores2  8410  tz7.44-3  8464  tz7.49c  8502  seqomlem2  8507  seqomlem3  8508  seqomlem4  8509  sbthlem4  9152  sbthlem6  9154  sbthlem8  9156  fodomfi  9378  pwfir  9383  fodomfiOLD  9398  dffi3  9500  marypha1lem  9502  marypha2lem4  9507  ordtypelem3  9589  ordtypelem9  9595  wdomima2g  9655  rankwflemb  9862  dfac8alem  10098  dfac12lem1  10213  zorn2lem1  10565  ttukeylem3  10580  imadomg  10603  iunfo  10608  fpwwe2lem5  10704  fpwwe2lem8  10707  fpwwe2lem12  10711  gruima  10871  peano5nni  12296  1nn  12304  peano2nn  12305  seqval  14063  hashimarn  14489  hashf1lem1  14504  frmdss2  18898  ghmima  19277  conjsubg  19290  gsumzaddlem  19963  gsumxp  20018  dprd2da  20086  dmdprdsplit2lem  20089  ablfac1b  20114  imadrhmcl  20820  pjdm  21750  lindsmm  21871  mplsubrglem  22047  tgrest  23188  cnconst2  23312  imacmp  23426  cmpfi  23437  connima  23454  kgencn3  23587  ptpjopn  23641  xkoccn  23648  txkgen  23681  qtoprest  23746  hmeores  23800  txflf  24035  subgntr  24136  opnsubg  24137  clsnsg  24139  tgpconncomp  24142  snclseqg  24145  tsmsf1o  24174  tsmsxplem1  24182  fmucndlem  24321  ovolicc2lem4  25574  mbflimsup  25720  itg1addlem4  25753  itg1addlem4OLD  25754  ellimc2  25932  c1lip3  26058  lhop  26075  dvcnvrelem1  26076  mdegfval  26121  aalioulem3  26394  taylthlem2  26434  taylthlem2OLD  26435  efifo  26607  dfrelog  26625  efopnlem2  26717  xrlimcnp  27029  fsumdvdsmul  27256  fsumdvdsmulOLD  27258  dchrghm  27318  madeval  27909  seqsval  28312  noseq0  28314  noseqp1  28315  noseqind  28316  om2noseqfo  28322  dfnns2  28380  uhgrspan1  29338  upgrreslem  29339  umgrreslem  29340  ex-ima  30474  imadifxp  32623  fresf1o  32650  imafi2  32725  ffsrn  32743  pfxrn3  32907  gsumzresunsn  33037  gsumhashmul  33040  cycpmconjvlem  33134  tocyccntz  33137  qusima  33401  lmimdim  33616  dimkerim  33640  mbfmcst  34224  0rrv  34416  cvmliftmolem1  35249  cvmlift2lem9a  35271  cvmlift2lem9  35279  mrsubff1o  35483  msubff1o  35525  rdgprc  35758  dfrdg2  35759  dfon4  35857  ivthALT  36301  mptsnunlem  37304  dissneqlem  37306  icoreelrnab  37320  icoreunrn  37325  poimirlem3  37583  poimirlem9  37589  poimirlem16  37596  poimirlem19  37599  poimirlem30  37610  cnres2  37723  rnresequniqs  38288  diaintclN  41015  dibintclN  41124  dihintcl  41301  imadomfi  41959  aks6d1c2  42087  aks6d1c6lem3  42129  imaopab  42224  imaiinfv  42649  diophrw  42715  dnnumch1  43001  fnwe2lem2  43008  hbtlem6  43086  imanonrel  43555  csbima12gALTVD  44868  imassmpt  45172  limsupvaluz  45629  funcoressn  46957  fcoreslem2  46979