Definition df-ima 5634

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 30534). Contrast with restriction (df-res 5633) and range (df-rn 5632). For an alternate definition, see dfima2 6021. (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 5624	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5623	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5622	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1548	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  5974  resima2  5975  elimampt  6002  imaeq1  6014  imaeq2  6015  dfima2  6021  nfima  6027  mptima  6031  rnresi  6034  resiima  6035  ima0  6036  imadisj  6039  imass1  6060  imass2  6061  imaundi  6104  imaundir  6105  imadifssran  6106  inimass  6110  rninxp  6134  imainrect  6136  xpima  6137  dfrn4  6157  imacnvcnv  6161  imadmres  6189  mptpreima  6193  rnco2  6209  resssxp  6225  funcnvres  6567  funimacnv  6570  f1imadifssran  6575  fnima  6619  fores  6753  f1ores  6785  f1orescnv  6786  foimacnv  6788  resdif  6792  rescnvimafod  7018  fvrnressn  7108  funfvima  7178  funiunfv  7196  soisores  7275  elimampo  7497  resfunexgALT  7894  curry1  8047  curry2  8050  fparlem3  8057  fparlem4  8058  fsplitfpar  8061  smores2  8288  tz7.44-3  8341  tz7.49c  8379  seqomlem2  8384  seqomlem3  8385  seqomlem4  8386  sbthlem4  9022  sbthlem6  9024  sbthlem8  9026  fodomfi  9216  pwfir  9221  fodomfiOLD  9234  imafi2  9265  dffi3  9338  marypha1lem  9340  marypha2lem4  9345  ordtypelem3  9429  ordtypelem9  9435  wdomima2g  9495  rankwflemb  9712  dfac8alem  9946  dfac12lem1  10061  zorn2lem1  10413  ttukeylem3  10428  imadomg  10451  iunfo  10456  fpwwe2lem5  10553  fpwwe2lem8  10556  fpwwe2lem12  10560  gruima  10720  peano5nni  12172  1nn  12180  peano2nn  12181  seqval  13969  hashimarn  14397  hashf1lem1  14412  frmdss2  18826  ghmima  19207  conjsubg  19220  gsumzaddlem  19891  gsumxp  19946  dprd2da  20014  dmdprdsplit2lem  20017  ablfac1b  20042  imadrhmcl  20773  pjdm  21686  lindsmm  21807  mplsubrglem  21982  tgrest  23146  cnconst2  23270  imacmp  23384  cmpfi  23395  connima  23412  kgencn3  23545  ptpjopn  23599  xkoccn  23606  txkgen  23639  qtoprest  23704  hmeores  23758  txflf  23993  subgntr  24094  opnsubg  24095  clsnsg  24097  tgpconncomp  24100  snclseqg  24103  tsmsf1o  24132  tsmsxplem1  24140  fmucndlem  24277  ovolicc2lem4  25509  mbflimsup  25655  itg1addlem4  25688  ellimc2  25866  c1lip3  25988  lhop  26005  dvcnvrelem1  26006  mdegfval  26049  aalioulem3  26322  taylthlem2  26361  efifo  26533  dfrelog  26551  efopnlem2  26643  xrlimcnp  26954  fsumdvdsmul  27180  dchrghm  27241  madeval  27846  seqsval  28302  noseq0  28304  noseqp1  28305  noseqind  28306  om2noseqfo  28312  dfnns2  28386  uhgrspan1  29394  upgrreslem  29395  umgrreslem  29396  ex-ima  30534  imadifxp  32694  fresf1o  32727  ffsrn  32824  pfxrn3  33024  gsumzresunsn  33147  gsumhashmul  33152  cycpmconjvlem  33226  tocyccntz  33229  qusima  33495  lmimdim  33800  dimkerim  33823  mbfmcst  34455  0rrv  34647  onvf1odlem3  35348  cvmliftmolem1  35524  cvmlift2lem9a  35546  cvmlift2lem9  35554  mrsubff1o  35758  msubff1o  35800  rdgprc  36035  dfrdg2  36036  dfon4  36134  ivthALT  36578  mptsnunlem  37715  dissneqlem  37717  icoreelrnab  37731  icoreunrn  37736  poimirlem3  38005  poimirlem9  38011  poimirlem16  38018  poimirlem19  38021  poimirlem30  38032  cnres2  38145  rnresequniqs  38716  diaintclN  41565  dibintclN  41674  dihintcl  41851  imadomfi  42502  aks6d1c2  42630  aks6d1c6lem3  42672  imaopab  42733  imaiinfv  43157  diophrw  43223  dnnumch1  43504  fnwe2lem2  43511  hbtlem6  43589  imanonrel  44052  csbima12gALTVD  45355  orbitinit  45415  orbitcl  45416  imassmpt  45720  limsupvaluz  46165  funcoressn  47519  fcoreslem2  47541