Definition df-ima 5654

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 30378). Contrast with restriction (df-res 5653) and range (df-rn 5652). For an alternate definition, see dfima2 6036. (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 5644	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5643	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5642	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1540	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  5989  resima2  5990  elimampt  6017  imaeq1  6029  imaeq2  6030  dfima2  6036  nfima  6042  mptima  6046  rnresi  6049  resiima  6050  ima0  6051  imadisj  6054  imass1  6075  imass2  6076  imaundi  6125  imaundir  6126  imadifssran  6127  inimass  6131  rninxp  6155  imainrect  6157  xpima  6158  dfrn4  6178  imacnvcnv  6182  imadmres  6210  mptpreima  6214  rnco2  6229  resssxp  6246  funcnvres  6597  funimacnv  6600  f1imadifssran  6605  fnima  6651  fores  6785  f1ores  6817  f1orescnv  6818  foimacnv  6820  resdif  6824  rescnvimafod  7048  fvrnressn  7136  funfvima  7207  funiunfv  7225  soisores  7305  elimampo  7529  resfunexgALT  7929  curry1  8086  curry2  8089  fparlem3  8096  fparlem4  8097  fsplitfpar  8100  smores2  8326  tz7.44-3  8379  tz7.49c  8417  seqomlem2  8422  seqomlem3  8423  seqomlem4  8424  sbthlem4  9060  sbthlem6  9062  sbthlem8  9064  fodomfi  9268  pwfir  9273  fodomfiOLD  9288  dffi3  9389  marypha1lem  9391  marypha2lem4  9396  ordtypelem3  9480  ordtypelem9  9486  wdomima2g  9546  rankwflemb  9753  dfac8alem  9989  dfac12lem1  10104  zorn2lem1  10456  ttukeylem3  10471  imadomg  10494  iunfo  10499  fpwwe2lem5  10595  fpwwe2lem8  10598  fpwwe2lem12  10602  gruima  10762  peano5nni  12196  1nn  12204  peano2nn  12205  seqval  13984  hashimarn  14412  hashf1lem1  14427  frmdss2  18797  ghmima  19176  conjsubg  19189  gsumzaddlem  19858  gsumxp  19913  dprd2da  19981  dmdprdsplit2lem  19984  ablfac1b  20009  imadrhmcl  20713  pjdm  21623  lindsmm  21744  mplsubrglem  21920  tgrest  23053  cnconst2  23177  imacmp  23291  cmpfi  23302  connima  23319  kgencn3  23452  ptpjopn  23506  xkoccn  23513  txkgen  23546  qtoprest  23611  hmeores  23665  txflf  23900  subgntr  24001  opnsubg  24002  clsnsg  24004  tgpconncomp  24007  snclseqg  24010  tsmsf1o  24039  tsmsxplem1  24047  fmucndlem  24185  ovolicc2lem4  25428  mbflimsup  25574  itg1addlem4  25607  ellimc2  25785  c1lip3  25911  lhop  25928  dvcnvrelem1  25929  mdegfval  25974  aalioulem3  26249  taylthlem2  26289  taylthlem2OLD  26290  efifo  26463  dfrelog  26481  efopnlem2  26573  xrlimcnp  26885  fsumdvdsmul  27112  fsumdvdsmulOLD  27114  dchrghm  27174  madeval  27767  seqsval  28189  noseq0  28191  noseqp1  28192  noseqind  28193  om2noseqfo  28199  dfnns2  28268  uhgrspan1  29237  upgrreslem  29238  umgrreslem  29239  ex-ima  30378  imadifxp  32537  fresf1o  32562  imafi2  32642  ffsrn  32659  pfxrn3  32869  gsumzresunsn  33003  gsumhashmul  33008  cycpmconjvlem  33105  tocyccntz  33108  qusima  33386  lmimdim  33606  dimkerim  33630  mbfmcst  34257  0rrv  34449  onvf1odlem3  35099  cvmliftmolem1  35275  cvmlift2lem9a  35297  cvmlift2lem9  35305  mrsubff1o  35509  msubff1o  35551  rdgprc  35789  dfrdg2  35790  dfon4  35888  ivthALT  36330  mptsnunlem  37333  dissneqlem  37335  icoreelrnab  37349  icoreunrn  37354  poimirlem3  37624  poimirlem9  37630  poimirlem16  37637  poimirlem19  37640  poimirlem30  37651  cnres2  37764  rnresequniqs  38323  diaintclN  41059  dibintclN  41168  dihintcl  41345  imadomfi  41997  aks6d1c2  42125  aks6d1c6lem3  42167  imaopab  42226  imaiinfv  42688  diophrw  42754  dnnumch1  43040  fnwe2lem2  43047  hbtlem6  43125  imanonrel  43589  csbima12gALTVD  44893  orbitinit  44953  orbitcl  44954  imassmpt  45263  limsupvaluz  45713  funcoressn  47047  fcoreslem2  47069