Definition df-ima 5667

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 30369). Contrast with restriction (df-res 5666) and range (df-rn 5665). For an alternate definition, see dfima2 6049. (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 5657	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5656	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5655	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1540	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  6002  resima2  6003  elimampt  6030  imaeq1  6042  imaeq2  6043  dfima2  6049  nfima  6055  mptima  6059  rnresi  6062  resiima  6063  ima0  6064  imadisj  6067  imass1  6088  imass2  6089  imaundi  6138  imaundir  6139  imadifssran  6140  inimass  6144  rninxp  6168  imainrect  6170  xpima  6171  dfrn4  6191  imacnvcnv  6195  imadmres  6223  mptpreima  6227  rnco2  6242  resssxp  6259  funcnvres  6613  funimacnv  6616  f1imadifssran  6621  fnima  6667  fores  6799  f1ores  6831  f1orescnv  6832  foimacnv  6834  resdif  6838  rescnvimafod  7062  fvrnressn  7150  funfvima  7221  funiunfv  7239  soisores  7319  elimampo  7542  resfunexgALT  7944  curry1  8101  curry2  8104  fparlem3  8111  fparlem4  8112  fsplitfpar  8115  smores2  8366  tz7.44-3  8420  tz7.49c  8458  seqomlem2  8463  seqomlem3  8464  seqomlem4  8465  sbthlem4  9098  sbthlem6  9100  sbthlem8  9102  fodomfi  9320  pwfir  9325  fodomfiOLD  9340  dffi3  9441  marypha1lem  9443  marypha2lem4  9448  ordtypelem3  9532  ordtypelem9  9538  wdomima2g  9598  rankwflemb  9805  dfac8alem  10041  dfac12lem1  10156  zorn2lem1  10508  ttukeylem3  10523  imadomg  10546  iunfo  10551  fpwwe2lem5  10647  fpwwe2lem8  10650  fpwwe2lem12  10654  gruima  10814  peano5nni  12241  1nn  12249  peano2nn  12250  seqval  14028  hashimarn  14456  hashf1lem1  14471  frmdss2  18839  ghmima  19218  conjsubg  19231  gsumzaddlem  19900  gsumxp  19955  dprd2da  20023  dmdprdsplit2lem  20026  ablfac1b  20051  imadrhmcl  20755  pjdm  21665  lindsmm  21786  mplsubrglem  21962  tgrest  23095  cnconst2  23219  imacmp  23333  cmpfi  23344  connima  23361  kgencn3  23494  ptpjopn  23548  xkoccn  23555  txkgen  23588  qtoprest  23653  hmeores  23707  txflf  23942  subgntr  24043  opnsubg  24044  clsnsg  24046  tgpconncomp  24049  snclseqg  24052  tsmsf1o  24081  tsmsxplem1  24089  fmucndlem  24227  ovolicc2lem4  25471  mbflimsup  25617  itg1addlem4  25650  ellimc2  25828  c1lip3  25954  lhop  25971  dvcnvrelem1  25972  mdegfval  26017  aalioulem3  26292  taylthlem2  26332  taylthlem2OLD  26333  efifo  26506  dfrelog  26524  efopnlem2  26616  xrlimcnp  26928  fsumdvdsmul  27155  fsumdvdsmulOLD  27157  dchrghm  27217  madeval  27808  seqsval  28211  noseq0  28213  noseqp1  28214  noseqind  28215  om2noseqfo  28221  dfnns2  28279  uhgrspan1  29228  upgrreslem  29229  umgrreslem  29230  ex-ima  30369  imadifxp  32528  fresf1o  32555  imafi2  32635  ffsrn  32652  pfxrn3  32862  gsumzresunsn  32996  gsumhashmul  33001  cycpmconjvlem  33098  tocyccntz  33101  qusima  33369  lmimdim  33589  dimkerim  33613  mbfmcst  34237  0rrv  34429  cvmliftmolem1  35249  cvmlift2lem9a  35271  cvmlift2lem9  35279  mrsubff1o  35483  msubff1o  35525  rdgprc  35758  dfrdg2  35759  dfon4  35857  ivthALT  36299  mptsnunlem  37302  dissneqlem  37304  icoreelrnab  37318  icoreunrn  37323  poimirlem3  37593  poimirlem9  37599  poimirlem16  37606  poimirlem19  37609  poimirlem30  37620  cnres2  37733  rnresequniqs  38296  diaintclN  41023  dibintclN  41132  dihintcl  41309  imadomfi  41961  aks6d1c2  42089  aks6d1c6lem3  42131  imaopab  42228  imaiinfv  42663  diophrw  42729  dnnumch1  43015  fnwe2lem2  43022  hbtlem6  43100  imanonrel  43564  csbima12gALTVD  44869  orbitinit  44929  orbitcl  44930  imassmpt  45234  limsupvaluz  45685  funcoressn  47019  fcoreslem2  47041