Definition df-ima 5698

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 30461). Contrast with restriction (df-res 5697) and range (df-rn 5696). For an alternate definition, see dfima2 6080. (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 5688	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5687	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5686	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1540	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  6033  resima2  6034  elimampt  6061  imaeq1  6073  imaeq2  6074  dfima2  6080  nfima  6086  mptima  6090  rnresi  6093  resiima  6094  ima0  6095  imadisj  6098  imass1  6119  imass2  6120  imaundi  6169  imaundir  6170  imadifssran  6171  inimass  6175  rninxp  6199  imainrect  6201  xpima  6202  dfrn4  6222  imacnvcnv  6226  imadmres  6254  mptpreima  6258  rnco2  6273  resssxp  6290  funcnvres  6644  funimacnv  6647  f1imadifssran  6652  fnima  6698  fores  6830  f1ores  6862  f1orescnv  6863  foimacnv  6865  resdif  6869  rescnvimafod  7093  fvrnressn  7181  funfvima  7250  funiunfv  7268  soisores  7347  elimampo  7570  resfunexgALT  7972  curry1  8129  curry2  8132  fparlem3  8139  fparlem4  8140  fsplitfpar  8143  smores2  8394  tz7.44-3  8448  tz7.49c  8486  seqomlem2  8491  seqomlem3  8492  seqomlem4  8493  sbthlem4  9126  sbthlem6  9128  sbthlem8  9130  fodomfi  9350  pwfir  9355  fodomfiOLD  9370  dffi3  9471  marypha1lem  9473  marypha2lem4  9478  ordtypelem3  9560  ordtypelem9  9566  wdomima2g  9626  rankwflemb  9833  dfac8alem  10069  dfac12lem1  10184  zorn2lem1  10536  ttukeylem3  10551  imadomg  10574  iunfo  10579  fpwwe2lem5  10675  fpwwe2lem8  10678  fpwwe2lem12  10682  gruima  10842  peano5nni  12269  1nn  12277  peano2nn  12278  seqval  14053  hashimarn  14479  hashf1lem1  14494  frmdss2  18876  ghmima  19255  conjsubg  19268  gsumzaddlem  19939  gsumxp  19994  dprd2da  20062  dmdprdsplit2lem  20065  ablfac1b  20090  imadrhmcl  20798  pjdm  21727  lindsmm  21848  mplsubrglem  22024  tgrest  23167  cnconst2  23291  imacmp  23405  cmpfi  23416  connima  23433  kgencn3  23566  ptpjopn  23620  xkoccn  23627  txkgen  23660  qtoprest  23725  hmeores  23779  txflf  24014  subgntr  24115  opnsubg  24116  clsnsg  24118  tgpconncomp  24121  snclseqg  24124  tsmsf1o  24153  tsmsxplem1  24161  fmucndlem  24300  ovolicc2lem4  25555  mbflimsup  25701  itg1addlem4  25734  ellimc2  25912  c1lip3  26038  lhop  26055  dvcnvrelem1  26056  mdegfval  26101  aalioulem3  26376  taylthlem2  26416  taylthlem2OLD  26417  efifo  26589  dfrelog  26607  efopnlem2  26699  xrlimcnp  27011  fsumdvdsmul  27238  fsumdvdsmulOLD  27240  dchrghm  27300  madeval  27891  seqsval  28294  noseq0  28296  noseqp1  28297  noseqind  28298  om2noseqfo  28304  dfnns2  28362  uhgrspan1  29320  upgrreslem  29321  umgrreslem  29322  ex-ima  30461  imadifxp  32614  fresf1o  32641  imafi2  32723  ffsrn  32740  pfxrn3  32925  gsumzresunsn  33059  gsumhashmul  33064  cycpmconjvlem  33161  tocyccntz  33164  qusima  33436  lmimdim  33654  dimkerim  33678  mbfmcst  34261  0rrv  34453  cvmliftmolem1  35286  cvmlift2lem9a  35308  cvmlift2lem9  35316  mrsubff1o  35520  msubff1o  35562  rdgprc  35795  dfrdg2  35796  dfon4  35894  ivthALT  36336  mptsnunlem  37339  dissneqlem  37341  icoreelrnab  37355  icoreunrn  37360  poimirlem3  37630  poimirlem9  37636  poimirlem16  37643  poimirlem19  37646  poimirlem30  37657  cnres2  37770  rnresequniqs  38333  diaintclN  41060  dibintclN  41169  dihintcl  41346  imadomfi  42003  aks6d1c2  42131  aks6d1c6lem3  42173  imaopab  42270  imaiinfv  42704  diophrw  42770  dnnumch1  43056  fnwe2lem2  43063  hbtlem6  43141  imanonrel  43606  csbima12gALTVD  44917  imassmpt  45269  limsupvaluz  45723  funcoressn  47054  fcoreslem2  47076