Definition df-ima 5695

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 30272). Contrast with restriction (df-res 5694) and range (df-rn 5693). For an alternate definition, see dfima2 6070. (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 5685	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5684	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5683	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1533	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  6024  resima2  6025  imaeq1  6063  imaeq2  6064  dfima2  6070  nfima  6076  mptima  6080  rnresi  6083  resiima  6084  ima0  6085  imadisj  6088  imass1  6110  imass2  6111  imaundi  6159  imaundir  6160  inimass  6164  rninxp  6188  imainrect  6190  xpima  6191  dfrn4  6211  imacnvcnv  6215  imadmres  6243  mptpreima  6247  rnco2  6262  resssxp  6279  funcnvres  6636  funimacnv  6639  fnima  6690  fores  6826  f1ores  6858  f1orescnv  6859  foimacnv  6861  resdif  6865  rescnvimafod  7088  fvrnressn  7176  funfvima  7248  funiunfv  7264  soisores  7341  elimampo  7564  resfunexgALT  7957  curry1  8115  curry2  8118  fparlem3  8125  fparlem4  8126  fsplitfpar  8129  smores2  8381  tz7.44-3  8435  tz7.49c  8473  seqomlem2  8478  seqomlem3  8479  seqomlem4  8480  sbthlem4  9117  sbthlem6  9119  sbthlem8  9121  pwfir  9207  fodomfi  9357  dffi3  9462  marypha1lem  9464  marypha2lem4  9469  ordtypelem3  9551  ordtypelem9  9557  wdomima2g  9617  rankwflemb  9824  dfac8alem  10060  dfac12lem1  10174  zorn2lem1  10527  ttukeylem3  10542  imadomg  10565  iunfo  10570  fpwwe2lem5  10666  fpwwe2lem8  10669  fpwwe2lem12  10673  gruima  10833  peano5nni  12253  1nn  12261  peano2nn  12262  seqval  14017  hashimarn  14439  hashf1lem1  14455  hashf1lem1OLD  14456  frmdss2  18822  ghmima  19198  conjsubg  19211  gsumzaddlem  19883  gsumxp  19938  dprd2da  20006  dmdprdsplit2lem  20009  ablfac1b  20034  rnrhmsubrg  20551  imadrhmcl  20692  pjdm  21648  lindsmm  21769  mplsubrglem  21953  tgrest  23083  cnconst2  23207  imacmp  23321  cmpfi  23332  connima  23349  kgencn3  23482  ptpjopn  23536  xkoccn  23543  txkgen  23576  qtoprest  23641  hmeores  23695  txflf  23930  subgntr  24031  opnsubg  24032  clsnsg  24034  tgpconncomp  24037  snclseqg  24040  tsmsf1o  24069  tsmsxplem1  24077  fmucndlem  24216  ovolicc2lem4  25469  mbflimsup  25615  itg1addlem4  25648  itg1addlem4OLD  25649  ellimc2  25826  c1lip3  25952  lhop  25969  dvcnvrelem1  25970  mdegfval  26018  aalioulem3  26289  taylthlem2  26329  taylthlem2OLD  26330  efifo  26501  dfrelog  26519  efopnlem2  26611  xrlimcnp  26920  fsumdvdsmul  27147  fsumdvdsmulOLD  27149  dchrghm  27209  madeval  27799  seqsval  28181  noseq0  28183  noseqp1  28184  noseqind  28185  om2noseqfo  28191  uhgrspan1  29136  upgrreslem  29137  umgrreslem  29138  ex-ima  30272  imadifxp  32412  fresf1o  32437  elimampt  32444  imafi2  32514  ffsrn  32532  pfxrn3  32685  gsumzresunsn  32789  gsumhashmul  32791  cycpmconjvlem  32883  tocyccntz  32886  qusima  33143  lmimdim  33334  dimkerim  33358  mbfmcst  33912  0rrv  34104  cvmliftmolem1  34924  cvmlift2lem9a  34946  cvmlift2lem9  34954  mrsubff1o  35158  msubff1o  35200  rdgprc  35423  dfrdg2  35424  dfon4  35522  ivthALT  35852  mptsnunlem  36850  dissneqlem  36852  icoreelrnab  36866  icoreunrn  36871  poimirlem3  37129  poimirlem9  37135  poimirlem16  37142  poimirlem19  37145  poimirlem30  37156  cnres2  37269  rnresequniqs  37836  diaintclN  40563  dibintclN  40672  dihintcl  40849  imadomfi  41505  aks6d1c2  41633  aks6d1c6lem3  41676  imaopab  41751  imaiinfv  42144  diophrw  42210  dnnumch1  42499  fnwe2lem2  42506  hbtlem6  42584  imanonrel  43054  csbima12gALTVD  44367  imassmpt  44668  limsupvaluz  45125  funcoressn  46453  fcoreslem2  46475