Definition df-ima 5663

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

This definition is used by:  elimampt  6034  imaeq1  6046  imaeq2  6047  imass1  6053  imass2  6054  resima  6055  resima2  6056  dfima2  6057  nfima  6063  mptima  6069  rnresi  6072  resiima  6073  ima0  6074  imadisj  6076  imaundi  6140  imaundir  6141  inimass  6144  rninxp  6170  imainrect  6172  xpima  6173  dfrn4  6196  imadifssrn  6201  imadifssranOLD  6202  imadifssranOLDOLD  6203  imacnvcnv  6207  imadmres  6235  mptpreima  6239  rnco2  6255  resssxp  6272  funcnvres  6618  funimacnv  6621  fnima  6669  fores  6806  f1ores  6839  f1orescnv  6840  foimacnv  6842  resdif  6846  rescnvimafod  7073  fvrnressn  7165  funfvima  7236  funiunfv  7252  soisores  7335  elimampo  7557  resfunexgALT  7960  curry1  8117  curry2  8120  fparlem3  8127  fparlem4  8128  fsplitfpar  8131  fnwe2lem3  8149  smores2  8365  tz7.44-3  8419  tz7.49c  8459  seqomlem2  8464  seqomlem3  8465  seqomlem4  8466  sbthlem4  9112  sbthlem6  9114  sbthlem8  9116  fodomfi  9307  pwfir  9311  imafi2  9353  dffi3  9426  marypha1lem  9428  marypha2lem4  9433  ordtypelem3  9517  ordtypelem9  9523  wdomima2g  9583  rankwflembOLD  9804  dfac8alem  10111  dfac12lem1  10225  zorn2lem1  10577  ttukeylem3  10592  imadomg  10616  imadomnum  10617  iunfo  10626  fpwwe2lem5  10723  fpwwe2lem8  10726  fpwwe2lem12  10730  gruima  10890  peano5nni  12341  1nn  12349  peano2nn  12350  seqval  14158  hashimarn  14588  hashf1lem1  14603  frmdss2  19064  ghmima  19456  conjsubg  19469  gsumzaddlem  20140  gsumxp  20195  dprd2da  20263  dmdprdsplit2lem  20266  ablfac1b  20291  imadrhmcl  21059  pjdm  22018  lindsmm  22139  mplsubrglem  22316  tgrest  23482  cnconst2  23606  imacmp  23720  cmpfi  23731  connima  23748  kgencn3  23882  ptpjopn  23936  xkoccn  23943  txkgen  23976  qtoprest  24041  hmeores  24095  txflf  24330  subgntr  24431  opnsubg  24432  clsnsg  24434  tgpconncomp  24437  snclseqg  24440  tsmsf1o  24469  tsmsxplem1  24477  fmucndlem  24614  ovolicc2lem4  25846  mbflimsup  25992  itg1addlem4  26025  ellimc2  26202  c1lip3  26324  lhop  26341  dvcnvrelem1  26342  mdegfval  26385  aalioulem3  26666  taylthlem2  26706  efifo  26880  dfrelog  26898  efopnlem2  26990  xrlimcnp  27301  fsumdvdsmul  27527  dchrghm  27588  madeval  28223  seqsval  28679  noseq0  28681  noseqp1  28682  noseqind  28683  om2noseqfo  28689  dfnns2  28763  uhgrspan1  29889  upgrreslem  29890  umgrreslem  29891  ex-ima  31048  imadifxp  33242  fresf1o  33272  ffsrn  33366  pfxrn3  33554  gsumzresunsn  33669  gsumhashmul  33674  cycpmconjvlem  33748  tocyccntz  33751  qusima  34005  lmimdim  34282  dimkerim  34305  mbfmcst  34937  0rrv  35129  onvf1odlem3  35952  cvmliftmolem1  36132  cvmlift2lem9a  36154  cvmlift2lem9  36162  mrsubff1o  36366  msubff1o  36408  rdgprc  36648  dfrdg2  36649  dfon4  36747  ivthALT  37215  mptsnunlem  38354  dissneqlem  38356  icoreelrnab  38370  icoreunrn  38375  poimirlem3  38634  poimirlem9  38640  poimirlem16  38647  poimirlem19  38650  poimirlem30  38661  cnres2  38790  rnresequniqs  39359  diaintclN  42208  dibintclN  42317  dihintcl  42494  imadomfi  43145  aks6d1c2  43273  aks6d1c6lem3  43315  imaopab  43378  imaiinfv  43797  diophrw  43863  dnnumch1  44144  hbtlem6  44224  imanonrel  44686  csbima12gALTVD  45972  orbitinit  46039  orbitcl  46040  imassmpt  46367  limsupvaluz  46811  funcoressn  48205  fcoreslem2  48227