Definition df-ima 5668

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

This definition is used by:  elimampt  6047  imaeq1  6059  imaeq2  6060  imass1  6066  imass2  6067  resima  6068  resima2  6069  dfima2  6070  nfima  6076  mptima  6082  rnresi  6085  resiima  6086  ima0  6087  imadisj  6089  imaundi  6153  imaundir  6154  inimass  6157  rninxp  6183  imainrect  6185  xpima  6186  dfrn4  6209  imadifssrn  6214  imadifssranOLD  6215  imadifssranOLDOLD  6216  imacnvcnv  6220  imadmres  6248  mptpreima  6252  rnco2  6268  resssxp  6290  funcnvres  6640  funimacnv  6643  fnima  6691  fores  6828  f1ores  6861  f1orescnv  6862  foimacnv  6864  resdif  6868  rescnvimafod  7097  fvrnressn  7189  funfvima  7259  funiunfv  7275  soisores  7358  elimampo  7581  resfunexgALT  7984  curry1  8142  curry2  8145  fparlem3  8152  fparlem4  8153  fsplitfpar  8156  fnwe2lem3  8174  smores2  8390  tz7.44-3  8444  tz7.49c  8484  seqomlem2  8489  seqomlem3  8490  seqomlem4  8491  sbthlem4  9137  sbthlem6  9139  sbthlem8  9141  fodomfi  9332  pwfir  9336  imafi2  9378  dffi3  9450  marypha1lem  9452  marypha2lem4  9457  ordtypelem3  9541  ordtypelem9  9547  wdomima2g  9607  rankwflembOLD  9828  dfac8alem  10135  dfac12lem1  10249  zorn2lem1  10601  ttukeylem3  10616  imadomg  10640  imadomnum  10641  iunfo  10650  fpwwe2lem5  10747  fpwwe2lem8  10750  fpwwe2lem12  10754  gruima  10914  peano5nni  12365  1nn  12373  peano2nn  12374  seqval  14182  hashimarn  14612  hashf1lem1  14627  frmdss2  19088  ghmima  19480  conjsubg  19493  gsumzaddlem  20165  gsumxp  20220  dprd2da  20288  dmdprdsplit2lem  20291  ablfac1b  20316  imadrhmcl  21084  pjdm  22043  lindsmm  22164  mplsubrglem  22341  tgrest  23507  cnconst2  23631  imacmp  23745  cmpfi  23756  connima  23773  kgencn3  23907  ptpjopn  23961  xkoccn  23968  txkgen  24001  qtoprest  24066  hmeores  24120  txflf  24355  subgntr  24456  opnsubg  24457  clsnsg  24459  tgpconncomp  24462  snclseqg  24465  tsmsf1o  24494  tsmsxplem1  24502  fmucndlem  24639  ovolicc2lem4  25871  mbflimsup  26017  itg1addlem4  26050  ellimc2  26227  c1lip3  26349  lhop  26366  dvcnvrelem1  26367  mdegfval  26410  aalioulem3  26691  taylthlem2  26731  efifo  26905  dfrelog  26923  efopnlem2  27015  xrlimcnp  27326  fsumdvdsmul  27552  dchrghm  27613  madeval  28248  seqsval  28704  noseq0  28706  noseqp1  28707  noseqind  28708  om2noseqfo  28714  dfnns2  28788  uhgrspan1  29914  upgrreslem  29915  umgrreslem  29916  ex-ima  31073  imadifxp  33267  fresf1o  33297  ffsrn  33390  pfxrn3  33578  gsumzresunsn  33693  gsumhashmul  33698  cycpmconjvlem  33772  tocyccntz  33775  qusima  34029  lmimdim  34306  dimkerim  34329  mbfmcst  34961  0rrv  35153  fnlfvk30  36027  onvf1odlem3  36033  cvmliftmolem1  36213  cvmlift2lem9a  36235  cvmlift2lem9  36243  mrsubff1o  36447  msubff1o  36489  rdgprc  36734  dfrdg2  36735  dfon4  36833  ivthALT  37301  mptsnunlem  38453  dissneqlem  38455  icoreelrnab  38469  icoreunrn  38474  poimirlem3  38733  poimirlem9  38739  poimirlem16  38746  poimirlem19  38749  poimirlem30  38760  cnres2  38889  rnresequniqs  39458  diaintclN  42307  dibintclN  42416  dihintcl  42593  imadomfi  43244  aks6d1c2  43372  aks6d1c6lem3  43414  imaopab  43478  imaiinfv  43897  diophrw  43963  dnnumch1  44244  hbtlem6  44323  imanonrel  44785  csbima12gALTVD  46070  orbitinit  46141  orbitcl  46142  imassmpt  46479  limsupvaluz  46923  funcoressn  48317  fcoreslem2  48339