Definition df-ima 5678

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 30389). Contrast with restriction (df-res 5677) and range (df-rn 5676). For an alternate definition, see dfima2 6060. (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 5668	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5667	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5666	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1539	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  6013  resima2  6014  elimampt  6041  imaeq1  6053  imaeq2  6054  dfima2  6060  nfima  6066  mptima  6070  rnresi  6073  resiima  6074  ima0  6075  imadisj  6078  imass1  6099  imass2  6100  imaundi  6149  imaundir  6150  imadifssran  6151  inimass  6155  rninxp  6179  imainrect  6181  xpima  6182  dfrn4  6202  imacnvcnv  6206  imadmres  6234  mptpreima  6238  rnco2  6253  resssxp  6270  funcnvres  6624  funimacnv  6627  f1imadifssran  6632  fnima  6678  fores  6810  f1ores  6842  f1orescnv  6843  foimacnv  6845  resdif  6849  rescnvimafod  7073  fvrnressn  7161  funfvima  7232  funiunfv  7250  soisores  7329  elimampo  7552  resfunexgALT  7954  curry1  8111  curry2  8114  fparlem3  8121  fparlem4  8122  fsplitfpar  8125  smores2  8376  tz7.44-3  8430  tz7.49c  8468  seqomlem2  8473  seqomlem3  8474  seqomlem4  8475  sbthlem4  9108  sbthlem6  9110  sbthlem8  9112  fodomfi  9332  pwfir  9337  fodomfiOLD  9352  dffi3  9453  marypha1lem  9455  marypha2lem4  9460  ordtypelem3  9542  ordtypelem9  9548  wdomima2g  9608  rankwflemb  9815  dfac8alem  10051  dfac12lem1  10166  zorn2lem1  10518  ttukeylem3  10533  imadomg  10556  iunfo  10561  fpwwe2lem5  10657  fpwwe2lem8  10660  fpwwe2lem12  10664  gruima  10824  peano5nni  12251  1nn  12259  peano2nn  12260  seqval  14035  hashimarn  14461  hashf1lem1  14476  frmdss2  18845  ghmima  19224  conjsubg  19237  gsumzaddlem  19907  gsumxp  19962  dprd2da  20030  dmdprdsplit2lem  20033  ablfac1b  20058  imadrhmcl  20766  pjdm  21681  lindsmm  21802  mplsubrglem  21978  tgrest  23113  cnconst2  23237  imacmp  23351  cmpfi  23362  connima  23379  kgencn3  23512  ptpjopn  23566  xkoccn  23573  txkgen  23606  qtoprest  23671  hmeores  23725  txflf  23960  subgntr  24061  opnsubg  24062  clsnsg  24064  tgpconncomp  24067  snclseqg  24070  tsmsf1o  24099  tsmsxplem1  24107  fmucndlem  24245  ovolicc2lem4  25491  mbflimsup  25637  itg1addlem4  25670  ellimc2  25848  c1lip3  25974  lhop  25991  dvcnvrelem1  25992  mdegfval  26037  aalioulem3  26312  taylthlem2  26352  taylthlem2OLD  26353  efifo  26525  dfrelog  26543  efopnlem2  26635  xrlimcnp  26947  fsumdvdsmul  27174  fsumdvdsmulOLD  27176  dchrghm  27236  madeval  27827  seqsval  28230  noseq0  28232  noseqp1  28233  noseqind  28234  om2noseqfo  28240  dfnns2  28298  uhgrspan1  29248  upgrreslem  29249  umgrreslem  29250  ex-ima  30389  imadifxp  32549  fresf1o  32576  imafi2  32658  ffsrn  32675  pfxrn3  32865  gsumzresunsn  32998  gsumhashmul  33003  cycpmconjvlem  33100  tocyccntz  33103  qusima  33371  lmimdim  33589  dimkerim  33613  mbfmcst  34220  0rrv  34412  cvmliftmolem1  35245  cvmlift2lem9a  35267  cvmlift2lem9  35275  mrsubff1o  35479  msubff1o  35521  rdgprc  35754  dfrdg2  35755  dfon4  35853  ivthALT  36295  mptsnunlem  37298  dissneqlem  37300  icoreelrnab  37314  icoreunrn  37319  poimirlem3  37589  poimirlem9  37595  poimirlem16  37602  poimirlem19  37605  poimirlem30  37616  cnres2  37729  rnresequniqs  38292  diaintclN  41019  dibintclN  41128  dihintcl  41305  imadomfi  41962  aks6d1c2  42090  aks6d1c6lem3  42132  imaopab  42229  imaiinfv  42667  diophrw  42733  dnnumch1  43019  fnwe2lem2  43026  hbtlem6  43104  imanonrel  43568  csbima12gALTVD  44874  imassmpt  45226  limsupvaluz  45680  funcoressn  47012  fcoreslem2  47034