Definition df-ima 5592

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 28682). Contrast with restriction (df-res 5591) and range (df-rn 5590). For an alternate definition, see dfima2 5959. (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 5582	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5581	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5580	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1543	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  5913  resima2  5914  imaeq1  5952  imaeq2  5953  dfima2  5959  nfima  5965  mptima  5969  rnresi  5971  resiima  5972  ima0  5973  imadisj  5976  imass1  5997  imass2  5998  imaundi  6041  imaundir  6042  inimass  6046  rninxp  6070  imainrect  6072  xpima  6073  dfrn4  6093  imacnvcnv  6097  imadmres  6125  mptpreima  6129  rnco2  6145  resssxp  6161  funcnvres  6493  funimacnv  6496  fnima  6544  fores  6679  f1ores  6711  f1orescnv  6712  foimacnv  6714  resdif  6717  rescnvimafod  6930  fvrnressn  7012  funfvima  7085  funiunfv  7100  soisores  7175  resfunexgALT  7761  curry1  7912  curry2  7915  fparlem3  7922  fparlem4  7923  fsplitfpar  7927  smores2  8133  tz7.44-3  8186  tz7.49c  8224  seqomlem2  8229  seqomlem3  8230  seqomlem4  8231  sbthlem4  8803  sbthlem6  8805  sbthlem8  8807  pwfir  8898  fodomfi  8997  dffi3  9095  marypha1lem  9097  marypha2lem4  9102  ordtypelem3  9184  ordtypelem9  9190  wdomima2g  9250  rankwflemb  9457  dfac8alem  9691  dfac12lem1  9805  zorn2lem1  10158  ttukeylem3  10173  imadomg  10196  iunfo  10201  fpwwe2lem5  10297  fpwwe2lem8  10300  fpwwe2lem12  10304  gruima  10464  peano5nni  11881  1nn  11889  peano2nn  11890  seqval  13635  hashimarn  14058  hashf1lem1  14071  hashf1lem1OLD  14072  frmdss2  18392  ghmima  18745  conjsubg  18756  gsumzaddlem  19412  gsumxp  19467  dprd2da  19535  dmdprdsplit2lem  19538  ablfac1b  19563  rnrhmsubrg  19946  pjdm  20799  lindsmm  20920  mplsubrglem  21095  tgrest  22193  cnconst2  22317  imacmp  22431  cmpfi  22442  connima  22459  kgencn3  22592  ptpjopn  22646  xkoccn  22653  txkgen  22686  qtoprest  22751  hmeores  22805  txflf  23040  subgntr  23141  opnsubg  23142  clsnsg  23144  tgpconncomp  23147  snclseqg  23150  tsmsf1o  23179  tsmsxplem1  23187  fmucndlem  23326  ovolicc2lem4  24564  mbflimsup  24710  itg1addlem4  24743  itg1addlem4OLD  24744  ellimc2  24921  c1lip3  25043  lhop  25060  dvcnvrelem1  25061  mdegfval  25107  aalioulem3  25374  taylthlem2  25413  efifo  25583  dfrelog  25601  efopnlem2  25692  xrlimcnp  25998  fsumdvdsmul  26224  dchrghm  26284  uhgrspan1  27548  upgrreslem  27549  umgrreslem  27550  ex-ima  28682  imadifxp  30816  fresf1o  30842  elimampt  30849  imafi2  30923  ffsrn  30941  pfxrn3  31092  gsumzresunsn  31191  gsumhashmul  31193  cycpmconjvlem  31285  tocyccntz  31288  qusima  31471  dimkerim  31585  mbfmcst  32101  0rrv  32293  cvmliftmolem1  33118  cvmlift2lem9a  33140  cvmlift2lem9  33148  mrsubff1o  33352  msubff1o  33394  rdgprc  33651  dfrdg2  33652  madeval  33938  dfon4  34097  ivthALT  34426  mptsnunlem  35415  dissneqlem  35417  icoreelrnab  35431  icoreunrn  35436  poimirlem3  35686  poimirlem9  35692  poimirlem16  35699  poimirlem19  35702  poimirlem30  35713  cnres2  35827  rnresequniqs  36373  diaintclN  38978  dibintclN  39087  dihintcl  39264  imaopab  40105  imaiinfv  40403  diophrw  40469  dnnumch1  40757  fnwe2lem2  40764  hbtlem6  40842  imanonrel  41062  csbima12gALTVD  42379  imassmpt  42672  limsupvaluz  43112  funcoressn  44396  fcoreslem2  44418