Definition df-ima 5568

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 28221). Contrast with restriction (df-res 5567) and range (df-rn 5566). For an alternate definition, see dfima2 5931. (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 5558	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5557	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5556	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1537	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  5887  resima2  5888  imaeq1  5924  imaeq2  5925  dfima2  5931  nfima  5937  mptima  5941  rnresi  5943  resiima  5944  ima0  5945  imadisj  5948  imass1  5964  imass2  5965  imaundi  6008  imaundir  6009  inimass  6012  rninxp  6036  imainrect  6038  xpima  6039  dfrn4  6059  imacnvcnv  6063  imadmres  6091  mptpreima  6092  rnco2  6106  funcnvres  6432  funimacnv  6435  fnima  6478  fores  6600  f1ores  6629  f1orescnv  6630  foimacnv  6632  resdif  6635  fvrnressn  6923  funfvima  6992  funiunfv  7007  soisores  7080  resfunexgALT  7649  curry1  7799  curry2  7802  fparlem3  7809  fparlem4  7810  fsplitfpar  7814  smores2  7991  tz7.44-3  8044  tz7.49c  8082  seqomlem2  8087  seqomlem3  8088  seqomlem4  8089  sbthlem4  8630  sbthlem6  8632  sbthlem8  8634  fodomfi  8797  dffi3  8895  marypha1lem  8897  marypha2lem4  8902  ordtypelem3  8984  ordtypelem9  8990  wdomima2g  9050  rankwflemb  9222  dfac8alem  9455  dfac12lem1  9569  zorn2lem1  9918  ttukeylem3  9933  imadomg  9956  iunfo  9961  fpwwe2lem6  10057  fpwwe2lem9  10060  fpwwe2lem13  10064  gruima  10224  peano5nni  11641  1nn  11649  peano2nn  11650  seqval  13381  hashimarn  13802  hashf1lem1  13814  frmdss2  18028  ghmima  18379  conjsubg  18390  gsumzaddlem  19041  gsumxp  19096  dprd2da  19164  dmdprdsplit2lem  19167  ablfac1b  19192  rnrhmsubrg  19567  mplsubrglem  20219  pjdm  20851  lindsmm  20972  tgrest  21767  cnconst2  21891  imacmp  22005  cmpfi  22016  connima  22033  kgencn3  22166  ptpjopn  22220  xkoccn  22227  txkgen  22260  qtoprest  22325  hmeores  22379  txflf  22614  subgntr  22715  opnsubg  22716  clsnsg  22718  tgpconncomp  22721  snclseqg  22724  tsmsf1o  22753  tsmsxplem1  22761  fmucndlem  22900  ovolicc2lem4  24121  mbflimsup  24267  itg1addlem4  24300  ellimc2  24475  c1lip3  24596  lhop  24613  dvcnvrelem1  24614  mdegfval  24656  aalioulem3  24923  taylthlem2  24962  efifo  25131  dfrelog  25149  efopnlem2  25240  xrlimcnp  25546  fsumdvdsmul  25772  dchrghm  25832  uhgrspan1  27085  upgrreslem  27086  umgrreslem  27087  ex-ima  28221  imadifxp  30351  fresf1o  30376  elimampt  30383  imafi2  30447  ffsrn  30465  pfxrn3  30617  gsumzresunsn  30691  cycpmconjvlem  30783  tocyccntz  30786  dimkerim  31023  mbfmcst  31517  0rrv  31709  cvmliftmolem1  32528  cvmlift2lem9a  32550  cvmlift2lem9  32558  mrsubff1o  32762  msubff1o  32804  rdgprc  33039  dfrdg2  33040  madeval  33289  dfon4  33354  ivthALT  33683  mptsnunlem  34622  dissneqlem  34624  icoreelrnab  34638  icoreunrn  34643  poimirlem3  34910  poimirlem9  34916  poimirlem16  34923  poimirlem19  34926  poimirlem30  34937  cnres2  35056  rnresequniqs  35604  diaintclN  38209  dibintclN  38318  dihintcl  38495  imaopab  39168  imaiinfv  39339  diophrw  39405  dnnumch1  39693  fnwe2lem2  39700  hbtlem6  39778  imanonrel  40002  rp-imass  40166  csbima12gALTVD  41280  imassmpt  41586  limsupvaluz  42038  funcoressn  43326