Definition df-ima 5645

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 30529). Contrast with restriction (df-res 5644) and range (df-rn 5643). For an alternate definition, see dfima2 6029. (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 5635	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5634	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5633	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1542	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  5982  resima2  5983  elimampt  6010  imaeq1  6022  imaeq2  6023  dfima2  6029  nfima  6035  mptima  6039  rnresi  6042  resiima  6043  ima0  6044  imadisj  6047  imass1  6068  imass2  6069  imaundi  6115  imaundir  6116  imadifssran  6117  inimass  6121  rninxp  6145  imainrect  6147  xpima  6148  dfrn4  6168  imacnvcnv  6172  imadmres  6200  mptpreima  6204  rnco2  6220  resssxp  6236  funcnvres  6578  funimacnv  6581  f1imadifssran  6586  fnima  6630  fores  6764  f1ores  6796  f1orescnv  6797  foimacnv  6799  resdif  6803  rescnvimafod  7027  fvrnressn  7116  funfvima  7186  funiunfv  7204  soisores  7283  elimampo  7505  resfunexgALT  7902  curry1  8056  curry2  8059  fparlem3  8066  fparlem4  8067  fsplitfpar  8070  smores2  8296  tz7.44-3  8349  tz7.49c  8387  seqomlem2  8392  seqomlem3  8393  seqomlem4  8394  sbthlem4  9030  sbthlem6  9032  sbthlem8  9034  fodomfi  9224  pwfir  9229  fodomfiOLD  9242  imafi2  9273  dffi3  9346  marypha1lem  9348  marypha2lem4  9353  ordtypelem3  9437  ordtypelem9  9443  wdomima2g  9503  rankwflemb  9717  dfac8alem  9951  dfac12lem1  10066  zorn2lem1  10418  ttukeylem3  10433  imadomg  10456  iunfo  10461  fpwwe2lem5  10558  fpwwe2lem8  10561  fpwwe2lem12  10565  gruima  10725  peano5nni  12160  1nn  12168  peano2nn  12169  seqval  13947  hashimarn  14375  hashf1lem1  14390  frmdss2  18800  ghmima  19178  conjsubg  19191  gsumzaddlem  19862  gsumxp  19917  dprd2da  19985  dmdprdsplit2lem  19988  ablfac1b  20013  imadrhmcl  20742  pjdm  21674  lindsmm  21795  mplsubrglem  21971  tgrest  23115  cnconst2  23239  imacmp  23353  cmpfi  23364  connima  23381  kgencn3  23514  ptpjopn  23568  xkoccn  23575  txkgen  23608  qtoprest  23673  hmeores  23727  txflf  23962  subgntr  24063  opnsubg  24064  clsnsg  24066  tgpconncomp  24069  snclseqg  24072  tsmsf1o  24101  tsmsxplem1  24109  fmucndlem  24246  ovolicc2lem4  25489  mbflimsup  25635  itg1addlem4  25668  ellimc2  25846  c1lip3  25972  lhop  25989  dvcnvrelem1  25990  mdegfval  26035  aalioulem3  26310  taylthlem2  26350  taylthlem2OLD  26351  efifo  26524  dfrelog  26542  efopnlem2  26634  xrlimcnp  26946  fsumdvdsmul  27173  fsumdvdsmulOLD  27175  dchrghm  27235  madeval  27840  seqsval  28296  noseq0  28298  noseqp1  28299  noseqind  28300  om2noseqfo  28306  dfnns2  28380  uhgrspan1  29388  upgrreslem  29389  umgrreslem  29390  ex-ima  30529  imadifxp  32687  fresf1o  32720  ffsrn  32817  pfxrn3  33033  gsumzresunsn  33155  gsumhashmul  33160  cycpmconjvlem  33234  tocyccntz  33237  qusima  33500  lmimdim  33780  dimkerim  33804  mbfmcst  34436  0rrv  34628  onvf1odlem3  35318  cvmliftmolem1  35494  cvmlift2lem9a  35516  cvmlift2lem9  35524  mrsubff1o  35728  msubff1o  35770  rdgprc  36005  dfrdg2  36006  dfon4  36104  ivthALT  36548  mptsnunlem  37582  dissneqlem  37584  icoreelrnab  37598  icoreunrn  37603  poimirlem3  37863  poimirlem9  37869  poimirlem16  37876  poimirlem19  37879  poimirlem30  37890  cnres2  38003  rnresequniqs  38574  diaintclN  41423  dibintclN  41532  dihintcl  41709  imadomfi  42361  aks6d1c2  42489  aks6d1c6lem3  42531  imaopab  42592  imaiinfv  43039  diophrw  43105  dnnumch1  43390  fnwe2lem2  43397  hbtlem6  43475  imanonrel  43938  csbima12gALTVD  45241  orbitinit  45301  orbitcl  45302  imassmpt  45609  limsupvaluz  46055  funcoressn  47391  fcoreslem2  47413