Definition df-ima 5532

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 28227). Contrast with restriction (df-res 5531) and range (df-rn 5530). For an alternate definition, see dfima2 5898. (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 5522	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5521	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5520	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1538	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  5852  resima2  5853  imaeq1  5891  imaeq2  5892  dfima2  5898  nfima  5904  mptima  5908  rnresi  5910  resiima  5911  ima0  5912  imadisj  5915  imass1  5931  imass2  5932  imaundi  5975  imaundir  5976  inimass  5979  rninxp  6003  imainrect  6005  xpima  6006  dfrn4  6026  imacnvcnv  6030  imadmres  6058  mptpreima  6059  rnco2  6073  resssxp  6089  funcnvres  6402  funimacnv  6405  fnima  6450  fores  6575  f1ores  6604  f1orescnv  6605  foimacnv  6607  resdif  6610  fvrnressn  6900  funfvima  6970  funiunfv  6985  soisores  7059  resfunexgALT  7631  curry1  7782  curry2  7785  fparlem3  7792  fparlem4  7793  fsplitfpar  7797  smores2  7974  tz7.44-3  8027  tz7.49c  8065  seqomlem2  8070  seqomlem3  8071  seqomlem4  8072  sbthlem4  8614  sbthlem6  8616  sbthlem8  8618  fodomfi  8781  dffi3  8879  marypha1lem  8881  marypha2lem4  8886  ordtypelem3  8968  ordtypelem9  8974  wdomima2g  9034  rankwflemb  9206  dfac8alem  9440  dfac12lem1  9554  zorn2lem1  9907  ttukeylem3  9922  imadomg  9945  iunfo  9950  fpwwe2lem6  10046  fpwwe2lem9  10049  fpwwe2lem13  10053  gruima  10213  peano5nni  11628  1nn  11636  peano2nn  11637  seqval  13375  hashimarn  13797  hashf1lem1  13809  frmdss2  18020  ghmima  18371  conjsubg  18382  gsumzaddlem  19034  gsumxp  19089  dprd2da  19157  dmdprdsplit2lem  19160  ablfac1b  19185  rnrhmsubrg  19560  pjdm  20396  lindsmm  20517  mplsubrglem  20677  tgrest  21764  cnconst2  21888  imacmp  22002  cmpfi  22013  connima  22030  kgencn3  22163  ptpjopn  22217  xkoccn  22224  txkgen  22257  qtoprest  22322  hmeores  22376  txflf  22611  subgntr  22712  opnsubg  22713  clsnsg  22715  tgpconncomp  22718  snclseqg  22721  tsmsf1o  22750  tsmsxplem1  22758  fmucndlem  22897  ovolicc2lem4  24124  mbflimsup  24270  itg1addlem4  24303  ellimc2  24480  c1lip3  24602  lhop  24619  dvcnvrelem1  24620  mdegfval  24663  aalioulem3  24930  taylthlem2  24969  efifo  25139  dfrelog  25157  efopnlem2  25248  xrlimcnp  25554  fsumdvdsmul  25780  dchrghm  25840  uhgrspan1  27093  upgrreslem  27094  umgrreslem  27095  ex-ima  28227  imadifxp  30364  fresf1o  30390  elimampt  30397  imafi2  30473  ffsrn  30491  pfxrn3  30643  gsumzresunsn  30739  gsumhashmul  30741  cycpmconjvlem  30833  tocyccntz  30836  dimkerim  31111  mbfmcst  31627  0rrv  31819  cvmliftmolem1  32641  cvmlift2lem9a  32663  cvmlift2lem9  32671  mrsubff1o  32875  msubff1o  32917  rdgprc  33152  dfrdg2  33153  madeval  33402  dfon4  33467  ivthALT  33796  mptsnunlem  34755  dissneqlem  34757  icoreelrnab  34771  icoreunrn  34776  poimirlem3  35060  poimirlem9  35066  poimirlem16  35073  poimirlem19  35076  poimirlem30  35087  cnres2  35201  rnresequniqs  35749  diaintclN  38354  dibintclN  38463  dihintcl  38640  imaopab  39413  imaiinfv  39634  diophrw  39700  dnnumch1  39988  fnwe2lem2  39995  hbtlem6  40073  imanonrel  40293  csbima12gALTVD  41603  imassmpt  41902  limsupvaluz  42350  funcoressn  43634