Definition df-ima 5701

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 30470). Contrast with restriction (df-res 5700) and range (df-rn 5699). For an alternate definition, see dfima2 6081. (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 5691	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5690	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5689	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1536	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  6034  resima2  6035  elimampt  6062  imaeq1  6074  imaeq2  6075  dfima2  6081  nfima  6087  mptima  6091  rnresi  6094  resiima  6095  ima0  6096  imadisj  6099  imass1  6121  imass2  6122  imaundi  6171  imaundir  6172  inimass  6176  rninxp  6200  imainrect  6202  xpima  6203  dfrn4  6223  imacnvcnv  6227  imadmres  6255  mptpreima  6259  rnco2  6274  resssxp  6291  funcnvres  6645  funimacnv  6648  fnima  6698  fores  6830  f1ores  6862  f1orescnv  6863  foimacnv  6865  resdif  6869  rescnvimafod  7092  fvrnressn  7180  funfvima  7249  funiunfv  7267  soisores  7346  elimampo  7569  resfunexgALT  7970  curry1  8127  curry2  8130  fparlem3  8137  fparlem4  8138  fsplitfpar  8141  smores2  8392  tz7.44-3  8446  tz7.49c  8484  seqomlem2  8489  seqomlem3  8490  seqomlem4  8491  sbthlem4  9124  sbthlem6  9126  sbthlem8  9128  fodomfi  9347  pwfir  9352  fodomfiOLD  9367  dffi3  9468  marypha1lem  9470  marypha2lem4  9475  ordtypelem3  9557  ordtypelem9  9563  wdomima2g  9623  rankwflemb  9830  dfac8alem  10066  dfac12lem1  10181  zorn2lem1  10533  ttukeylem3  10548  imadomg  10571  iunfo  10576  fpwwe2lem5  10672  fpwwe2lem8  10675  fpwwe2lem12  10679  gruima  10839  peano5nni  12266  1nn  12274  peano2nn  12275  seqval  14049  hashimarn  14475  hashf1lem1  14490  frmdss2  18888  ghmima  19267  conjsubg  19280  gsumzaddlem  19953  gsumxp  20008  dprd2da  20076  dmdprdsplit2lem  20079  ablfac1b  20104  imadrhmcl  20814  pjdm  21744  lindsmm  21865  mplsubrglem  22041  tgrest  23182  cnconst2  23306  imacmp  23420  cmpfi  23431  connima  23448  kgencn3  23581  ptpjopn  23635  xkoccn  23642  txkgen  23675  qtoprest  23740  hmeores  23794  txflf  24029  subgntr  24130  opnsubg  24131  clsnsg  24133  tgpconncomp  24136  snclseqg  24139  tsmsf1o  24168  tsmsxplem1  24176  fmucndlem  24315  ovolicc2lem4  25568  mbflimsup  25714  itg1addlem4  25747  itg1addlem4OLD  25748  ellimc2  25926  c1lip3  26052  lhop  26069  dvcnvrelem1  26070  mdegfval  26115  aalioulem3  26390  taylthlem2  26430  taylthlem2OLD  26431  efifo  26603  dfrelog  26621  efopnlem2  26713  xrlimcnp  27025  fsumdvdsmul  27252  fsumdvdsmulOLD  27254  dchrghm  27314  madeval  27905  seqsval  28308  noseq0  28310  noseqp1  28311  noseqind  28312  om2noseqfo  28318  dfnns2  28376  uhgrspan1  29334  upgrreslem  29335  umgrreslem  29336  ex-ima  30470  imadifxp  32620  fresf1o  32647  imafi2  32728  ffsrn  32746  pfxrn3  32909  gsumzresunsn  33041  gsumhashmul  33046  cycpmconjvlem  33143  tocyccntz  33146  qusima  33415  lmimdim  33630  dimkerim  33654  mbfmcst  34240  0rrv  34432  cvmliftmolem1  35265  cvmlift2lem9a  35287  cvmlift2lem9  35295  mrsubff1o  35499  msubff1o  35541  rdgprc  35775  dfrdg2  35776  dfon4  35874  ivthALT  36317  mptsnunlem  37320  dissneqlem  37322  icoreelrnab  37336  icoreunrn  37341  poimirlem3  37609  poimirlem9  37615  poimirlem16  37622  poimirlem19  37625  poimirlem30  37636  cnres2  37749  rnresequniqs  38313  diaintclN  41040  dibintclN  41149  dihintcl  41326  imadomfi  41983  aks6d1c2  42111  aks6d1c6lem3  42153  imaopab  42248  imaiinfv  42680  diophrw  42746  dnnumch1  43032  fnwe2lem2  43039  hbtlem6  43117  imanonrel  43582  csbima12gALTVD  44894  imassmpt  45207  limsupvaluz  45663  funcoressn  46991  fcoreslem2  47013