Definition df-ima 5127

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 27299). Contrast with restriction (df-res 5126) and range (df-rn 5125). For an alternate definition, see dfima2 5468. (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 5117	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5116	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5115	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1483	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  5431  resima2  5432  resima2OLD  5433  imaeq1  5461  imaeq2  5462  dfima2  5468  nfima  5474  rnresi  5479  resiima  5480  ima0  5481  imadisj  5484  imass1  5500  imass2  5501  imaundi  5545  imaundir  5546  inimass  5549  rninxp  5573  imainrect  5575  xpima  5576  dfrn4  5595  imacnvcnv  5599  imadmres  5627  mptpreima  5628  rnco2  5642  funcnvres  5967  funimacnv  5970  fnima  6010  fores  6124  f1ores  6151  f1orescnv  6152  foimacnv  6154  resdif  6157  fvrnressn  6428  funfvima  6492  funiunfv  6506  soisores  6577  resfunexgALT  7129  curry1  7269  curry2  7272  fparlem3  7279  fparlem4  7280  smores2  7451  tz7.44-3  7504  tz7.49c  7541  seqomlem2  7546  seqomlem3  7547  seqomlem4  7548  sbthlem4  8073  sbthlem6  8075  sbthlem8  8077  fodomfi  8239  dffi3  8337  marypha1lem  8339  marypha2lem4  8344  ordtypelem3  8425  ordtypelem9  8431  wdomima2g  8491  rankwflemb  8656  dfac8alem  8852  dfac12lem1  8965  zorn2lem1  9318  ttukeylem3  9333  imadomg  9356  iunfo  9361  fpwwe2lem6  9457  fpwwe2lem9  9460  fpwwe2lem13  9464  gruima  9624  peano5nni  11023  1nn  11031  peano2nn  11032  seqval  12812  hashimarn  13227  hashf1lem1  13239  frmdss2  17400  ghmima  17681  conjsubg  17692  gsumzaddlem  18321  gsumxp  18375  dprd2da  18441  dmdprdsplit2lem  18444  ablfac1b  18469  mplsubrglem  19439  pjdm  20051  lindsmm  20167  tgrest  20963  cnconst2  21087  imacmp  21200  cmpfi  21211  connima  21228  kgencn3  21361  ptpjopn  21415  xkoccn  21422  txkgen  21455  qtoprest  21520  hmeores  21574  txflf  21810  subgntr  21910  opnsubg  21911  clsnsg  21913  tgpconncomp  21916  snclseqg  21919  tsmsf1o  21948  tsmsxplem1  21956  fmucndlem  22095  ovolicc2lem4  23288  mbflimsup  23433  itg1addlem4  23466  ellimc2  23641  c1lip3  23762  lhop  23779  dvcnvrelem1  23780  mdegfval  23822  aalioulem3  24089  taylthlem2  24128  efifo  24293  dfrelog  24312  efopnlem2  24403  xrlimcnp  24695  fsumdvdsmul  24921  dchrghm  24981  uhgrspan1  26195  upgrreslem  26196  umgrreslem  26197  ex-ima  27299  imadifxp  29414  fresf1o  29433  elimampt  29438  imafi2  29489  ffsrn  29504  mbfmcst  30321  0rrv  30513  cvmliftmolem1  31263  cvmlift2lem9a  31285  cvmlift2lem9  31293  mrsubff1o  31412  msubff1o  31454  rdgprc  31700  dfrdg2  31701  madeval  31935  dfon4  32000  ivthALT  32330  mptsnunlem  33185  dissneqlem  33187  icoreelrnab  33202  icoreunrn  33207  poimirlem3  33412  poimirlem9  33418  poimirlem16  33425  poimirlem19  33428  poimirlem30  33439  cnres2  33562  rnresequniqs  34102  diaintclN  36347  dibintclN  36456  dihintcl  36633  imaiinfv  37256  diophrw  37322  dnnumch1  37614  fnwe2lem2  37621  hbtlem6  37699  imanonrel  37899  rp-imass  38065  csbima12gALTOLD  39057  csbima12gALTVD  39133  mptima  39437  imassmpt  39481  limsupvaluz  39940  funcoressn  41207