Definition df-ima 5672

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 30930). Contrast with restriction (df-res 5671) and range (df-rn 5670). For an alternate definition, see dfima2 6062. (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 5662	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5661	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5660	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1570	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is used by:  resima  6012  resima2  6013  elimampt  6043  imaeq1  6055  imaeq2  6056  dfima2  6062  nfima  6068  mptima  6072  rnresi  6075  resiima  6076  ima0  6077  imadisj  6080  imass1  6101  imass2  6102  imaundi  6145  imaundir  6146  inimass  6150  rninxp  6176  imainrect  6178  xpima  6179  dfrn4  6200  imadifssran  6201  imadifssranOLD  6202  imacnvcnv  6206  imadmres  6234  mptpreima  6238  rnco2  6254  resssxp  6271  funcnvres  6615  funimacnv  6618  fnima  6666  fores  6803  f1ores  6836  f1orescnv  6837  foimacnv  6839  resdif  6843  rescnvimafod  7070  fvrnressn  7162  funfvima  7233  funiunfv  7249  soisores  7332  elimampo  7554  resfunexgALT  7949  curry1  8105  curry2  8108  fparlem3  8115  fparlem4  8116  fsplitfpar  8119  smores2  8347  tz7.44-3  8401  tz7.49c  8439  seqomlem2  8444  seqomlem3  8445  seqomlem4  8446  sbthlem4  9092  sbthlem6  9094  sbthlem8  9096  fodomfi  9286  pwfir  9290  imafi2  9332  dffi3  9405  marypha1lem  9407  marypha2lem4  9412  ordtypelem3  9496  ordtypelem9  9502  wdomima2g  9562  rankwflemb  9779  dfac8alem  10036  dfac12lem1  10150  zorn2lem1  10502  ttukeylem3  10517  imadomg  10541  imadomnum  10542  iunfo  10551  fpwwe2lem5  10648  fpwwe2lem8  10651  fpwwe2lem12  10655  gruima  10815  peano5nni  12264  1nn  12272  peano2nn  12273  seqval  14080  hashimarn  14509  hashf1lem1  14524  frmdss2  18978  ghmima  19370  conjsubg  19383  gsumzaddlem  20054  gsumxp  20109  dprd2da  20177  dmdprdsplit2lem  20180  ablfac1b  20205  imadrhmcl  20969  pjdm  21926  lindsmm  22047  mplsubrglem  22224  tgrest  23390  cnconst2  23514  imacmp  23628  cmpfi  23639  connima  23656  kgencn3  23790  ptpjopn  23844  xkoccn  23851  txkgen  23884  qtoprest  23949  hmeores  24003  txflf  24238  subgntr  24339  opnsubg  24340  clsnsg  24342  tgpconncomp  24345  snclseqg  24348  tsmsf1o  24377  tsmsxplem1  24385  fmucndlem  24522  ovolicc2lem4  25754  mbflimsup  25900  itg1addlem4  25933  ellimc2  26111  c1lip3  26233  lhop  26250  dvcnvrelem1  26251  mdegfval  26294  aalioulem3  26577  taylthlem2  26617  efifo  26792  dfrelog  26810  efopnlem2  26902  xrlimcnp  27213  fsumdvdsmul  27439  dchrghm  27500  madeval  28105  seqsval  28561  noseq0  28563  noseqp1  28564  noseqind  28565  om2noseqfo  28571  dfnns2  28645  uhgrspan1  29771  upgrreslem  29772  umgrreslem  29773  ex-ima  30930  imadifxp  33082  fresf1o  33112  ffsrn  33207  pfxrn3  33395  gsumzresunsn  33510  gsumhashmul  33515  cycpmconjvlem  33589  tocyccntz  33592  qusima  33845  lmimdim  34122  dimkerim  34145  mbfmcst  34778  0rrv  34970  onvf1odlem3  35710  cvmliftmolem1  35868  cvmlift2lem9a  35890  cvmlift2lem9  35898  mrsubff1o  36102  msubff1o  36144  rdgprc  36379  dfrdg2  36380  dfon4  36478  ivthALT  36962  mptsnunlem  38100  dissneqlem  38102  icoreelrnab  38116  icoreunrn  38121  poimirlem3  38380  poimirlem9  38386  poimirlem16  38393  poimirlem19  38396  poimirlem30  38407  cnres2  38521  rnresequniqs  39090  diaintclN  41939  dibintclN  42048  dihintcl  42225  imadomfi  42876  aks6d1c2  43004  aks6d1c6lem3  43046  imaopab  43109  imaiinfv  43546  diophrw  43612  dnnumch1  43893  fnwe2lem2  43900  hbtlem6  43978  imanonrel  44441  csbima12gALTVD  45727  orbitinit  45787  orbitcl  45788  imassmpt  46099  limsupvaluz  46544  funcoressn  47938  fcoreslem2  47960