Definition df-ima 5665

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 30702). Contrast with restriction (df-res 5664) and range (df-rn 5663). For an alternate definition, see dfima2 6055. (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 5655	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5654	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5653	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1563	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  6005  resima2  6006  elimampt  6036  imaeq1  6048  imaeq2  6049  dfima2  6055  nfima  6061  mptima  6065  rnresi  6068  resiima  6069  ima0  6070  imadisj  6073  imass1  6094  imass2  6095  imaundi  6138  imaundir  6139  imadifssran  6140  inimass  6144  rninxp  6169  imainrect  6171  xpima  6172  dfrn4  6193  imacnvcnv  6197  imadmres  6225  mptpreima  6229  rnco2  6245  resssxp  6261  funcnvres  6603  funimacnv  6606  f1imadifssran  6611  fnima  6655  fores  6792  f1ores  6825  f1orescnv  6826  foimacnv  6828  resdif  6832  rescnvimafod  7058  fvrnressn  7148  funfvima  7218  funiunfv  7236  soisores  7315  elimampo  7537  resfunexgALT  7933  curry1  8087  curry2  8090  fparlem3  8097  fparlem4  8098  fsplitfpar  8101  smores2  8329  tz7.44-3  8383  tz7.49c  8421  seqomlem2  8426  seqomlem3  8427  seqomlem4  8428  sbthlem4  9066  sbthlem6  9068  sbthlem8  9070  fodomfi  9260  pwfir  9264  imafi2  9306  dffi3  9379  marypha1lem  9381  marypha2lem4  9386  ordtypelem3  9470  ordtypelem9  9476  wdomima2g  9536  rankwflemb  9753  dfac8alem  10001  dfac12lem1  10115  zorn2lem1  10468  ttukeylem3  10483  imadomg  10506  iunfo  10511  fpwwe2lem5  10608  fpwwe2lem8  10611  fpwwe2lem12  10615  gruima  10775  peano5nni  12227  1nn  12235  peano2nn  12236  seqval  14039  hashimarn  14467  hashf1lem1  14482  frmdss2  18912  ghmima  19298  conjsubg  19311  gsumzaddlem  19982  gsumxp  20037  dprd2da  20105  dmdprdsplit2lem  20108  ablfac1b  20133  imadrhmcl  20869  pjdm  21817  lindsmm  21938  mplsubrglem  22113  tgrest  23277  cnconst2  23401  imacmp  23515  cmpfi  23526  connima  23543  kgencn3  23676  ptpjopn  23730  xkoccn  23737  txkgen  23770  qtoprest  23835  hmeores  23889  txflf  24124  subgntr  24225  opnsubg  24226  clsnsg  24228  tgpconncomp  24231  snclseqg  24234  tsmsf1o  24263  tsmsxplem1  24271  fmucndlem  24408  ovolicc2lem4  25640  mbflimsup  25786  itg1addlem4  25819  ellimc2  25997  c1lip3  26119  lhop  26136  dvcnvrelem1  26137  mdegfval  26180  aalioulem3  26456  taylthlem2  26495  efifo  26670  dfrelog  26688  efopnlem2  26780  xrlimcnp  27091  fsumdvdsmul  27317  dchrghm  27378  madeval  27983  seqsval  28439  noseq0  28441  noseqp1  28442  noseqind  28443  om2noseqfo  28449  dfnns2  28523  uhgrspan1  29562  upgrreslem  29563  umgrreslem  29564  ex-ima  30702  imadifxp  32856  fresf1o  32888  ffsrn  32985  pfxrn3  33174  gsumzresunsn  33295  gsumhashmul  33300  cycpmconjvlem  33374  tocyccntz  33377  qusima  33633  lmimdim  33911  dimkerim  33934  mbfmcst  34566  0rrv  34758  onvf1odlem3  35460  cvmliftmolem1  35644  cvmlift2lem9a  35666  cvmlift2lem9  35674  mrsubff1o  35878  msubff1o  35920  rdgprc  36155  dfrdg2  36156  dfon4  36254  ivthALT  36708  mptsnunlem  37844  dissneqlem  37846  icoreelrnab  37860  icoreunrn  37865  poimirlem3  38134  poimirlem9  38140  poimirlem16  38147  poimirlem19  38150  poimirlem30  38161  cnres2  38274  rnresequniqs  38845  diaintclN  41694  dibintclN  41803  dihintcl  41980  imadomfi  42631  aks6d1c2  42759  aks6d1c6lem3  42801  imaopab  42862  imaiinfv  43286  diophrw  43352  dnnumch1  43633  fnwe2lem2  43640  hbtlem6  43718  imanonrel  44181  csbima12gALTVD  45470  orbitinit  45530  orbitcl  45531  imassmpt  45835  limsupvaluz  46280  funcoressn  47634  fcoreslem2  47656