Definition df-ima 5664

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

This definition is used by:  resima  6006  resima2  6007  elimampt  6037  imaeq1  6049  imaeq2  6050  dfima2  6056  nfima  6062  mptima  6066  rnresi  6069  resiima  6070  ima0  6071  imadisj  6074  imass1  6095  imass2  6096  imaundi  6139  imaundir  6140  inimass  6144  rninxp  6170  imainrect  6172  xpima  6173  dfrn4  6194  imadifssran  6195  imadifssranOLD  6196  imacnvcnv  6200  imadmres  6228  mptpreima  6232  rnco2  6248  resssxp  6265  funcnvres  6610  funimacnv  6613  fnima  6661  fores  6798  f1ores  6831  f1orescnv  6832  foimacnv  6834  resdif  6838  rescnvimafod  7065  fvrnressn  7157  funfvima  7228  funiunfv  7244  soisores  7327  elimampo  7549  resfunexgALT  7949  curry1  8104  curry2  8107  fparlem3  8114  fparlem4  8115  fsplitfpar  8118  smores2  8346  tz7.44-3  8400  tz7.49c  8440  seqomlem2  8445  seqomlem3  8446  seqomlem4  8447  sbthlem4  9093  sbthlem6  9095  sbthlem8  9097  fodomfi  9288  pwfir  9292  imafi2  9334  dffi3  9407  marypha1lem  9409  marypha2lem4  9414  ordtypelem3  9498  ordtypelem9  9504  wdomima2g  9564  rankwflemb  9781  dfac8alem  10086  dfac12lem1  10200  zorn2lem1  10552  ttukeylem3  10567  imadomg  10591  imadomnum  10592  iunfo  10601  fpwwe2lem5  10698  fpwwe2lem8  10701  fpwwe2lem12  10705  gruima  10865  peano5nni  12316  1nn  12324  peano2nn  12325  seqval  14132  hashimarn  14562  hashf1lem1  14577  frmdss2  19036  ghmima  19428  conjsubg  19441  gsumzaddlem  20112  gsumxp  20167  dprd2da  20235  dmdprdsplit2lem  20238  ablfac1b  20263  imadrhmcl  21031  pjdm  21990  lindsmm  22111  mplsubrglem  22288  tgrest  23454  cnconst2  23578  imacmp  23692  cmpfi  23703  connima  23720  kgencn3  23854  ptpjopn  23908  xkoccn  23915  txkgen  23948  qtoprest  24013  hmeores  24067  txflf  24302  subgntr  24403  opnsubg  24404  clsnsg  24406  tgpconncomp  24409  snclseqg  24412  tsmsf1o  24441  tsmsxplem1  24449  fmucndlem  24586  ovolicc2lem4  25818  mbflimsup  25964  itg1addlem4  25997  ellimc2  26174  c1lip3  26296  lhop  26313  dvcnvrelem1  26314  mdegfval  26357  aalioulem3  26640  taylthlem2  26680  efifo  26854  dfrelog  26872  efopnlem2  26964  xrlimcnp  27275  fsumdvdsmul  27501  dchrghm  27562  madeval  28197  seqsval  28653  noseq0  28655  noseqp1  28656  noseqind  28657  om2noseqfo  28663  dfnns2  28737  uhgrspan1  29863  upgrreslem  29864  umgrreslem  29865  ex-ima  31022  imadifxp  33174  fresf1o  33204  ffsrn  33299  pfxrn3  33487  gsumzresunsn  33602  gsumhashmul  33607  cycpmconjvlem  33681  tocyccntz  33684  qusima  33938  lmimdim  34215  dimkerim  34238  mbfmcst  34871  0rrv  35063  onvf1odlem3  35854  cvmliftmolem1  36012  cvmlift2lem9a  36034  cvmlift2lem9  36042  mrsubff1o  36246  msubff1o  36288  rdgprc  36523  dfrdg2  36524  dfon4  36622  ivthALT  37090  mptsnunlem  38226  dissneqlem  38228  icoreelrnab  38242  icoreunrn  38247  poimirlem3  38506  poimirlem9  38512  poimirlem16  38519  poimirlem19  38522  poimirlem30  38533  cnres2  38662  rnresequniqs  39231  diaintclN  42080  dibintclN  42189  dihintcl  42366  imadomfi  43017  aks6d1c2  43145  aks6d1c6lem3  43187  imaopab  43250  imaiinfv  43654  diophrw  43720  dnnumch1  44001  fnwe2lem2  44008  hbtlem6  44086  imanonrel  44549  csbima12gALTVD  45835  orbitinit  45895  orbitcl  45896  imassmpt  46214  limsupvaluz  46659  funcoressn  48053  fcoreslem2  48075