Definition df-ima 5602

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 28806). Contrast with restriction (df-res 5601) and range (df-rn 5600). For an alternate definition, see dfima2 5971. (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 5592	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5591	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5590	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1539	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  5925  resima2  5926  imaeq1  5964  imaeq2  5965  dfima2  5971  nfima  5977  mptima  5981  rnresi  5983  resiima  5984  ima0  5985  imadisj  5988  imass1  6009  imass2  6010  imaundi  6053  imaundir  6054  inimass  6058  rninxp  6082  imainrect  6084  xpima  6085  dfrn4  6105  imacnvcnv  6109  imadmres  6137  mptpreima  6141  rnco2  6157  resssxp  6173  funcnvres  6512  funimacnv  6515  fnima  6563  fores  6698  f1ores  6730  f1orescnv  6731  foimacnv  6733  resdif  6737  rescnvimafod  6951  fvrnressn  7033  funfvima  7106  funiunfv  7121  soisores  7198  resfunexgALT  7790  curry1  7944  curry2  7947  fparlem3  7954  fparlem4  7955  fsplitfpar  7959  smores2  8185  tz7.44-3  8239  tz7.49c  8277  seqomlem2  8282  seqomlem3  8283  seqomlem4  8284  sbthlem4  8873  sbthlem6  8875  sbthlem8  8877  pwfir  8959  fodomfi  9092  dffi3  9190  marypha1lem  9192  marypha2lem4  9197  ordtypelem3  9279  ordtypelem9  9285  wdomima2g  9345  rankwflemb  9551  dfac8alem  9785  dfac12lem1  9899  zorn2lem1  10252  ttukeylem3  10267  imadomg  10290  iunfo  10295  fpwwe2lem5  10391  fpwwe2lem8  10394  fpwwe2lem12  10398  gruima  10558  peano5nni  11976  1nn  11984  peano2nn  11985  seqval  13732  hashimarn  14155  hashf1lem1  14168  hashf1lem1OLD  14169  frmdss2  18502  ghmima  18855  conjsubg  18866  gsumzaddlem  19522  gsumxp  19577  dprd2da  19645  dmdprdsplit2lem  19648  ablfac1b  19673  rnrhmsubrg  20056  pjdm  20914  lindsmm  21035  mplsubrglem  21210  tgrest  22310  cnconst2  22434  imacmp  22548  cmpfi  22559  connima  22576  kgencn3  22709  ptpjopn  22763  xkoccn  22770  txkgen  22803  qtoprest  22868  hmeores  22922  txflf  23157  subgntr  23258  opnsubg  23259  clsnsg  23261  tgpconncomp  23264  snclseqg  23267  tsmsf1o  23296  tsmsxplem1  23304  fmucndlem  23443  ovolicc2lem4  24684  mbflimsup  24830  itg1addlem4  24863  itg1addlem4OLD  24864  ellimc2  25041  c1lip3  25163  lhop  25180  dvcnvrelem1  25181  mdegfval  25227  aalioulem3  25494  taylthlem2  25533  efifo  25703  dfrelog  25721  efopnlem2  25812  xrlimcnp  26118  fsumdvdsmul  26344  dchrghm  26404  uhgrspan1  27670  upgrreslem  27671  umgrreslem  27672  ex-ima  28806  imadifxp  30940  fresf1o  30966  elimampt  30973  imafi2  31046  ffsrn  31064  pfxrn3  31215  gsumzresunsn  31314  gsumhashmul  31316  cycpmconjvlem  31408  tocyccntz  31411  qusima  31594  dimkerim  31708  mbfmcst  32226  0rrv  32418  cvmliftmolem1  33243  cvmlift2lem9a  33265  cvmlift2lem9  33273  mrsubff1o  33477  msubff1o  33519  rdgprc  33770  dfrdg2  33771  madeval  34036  dfon4  34195  ivthALT  34524  mptsnunlem  35509  dissneqlem  35511  icoreelrnab  35525  icoreunrn  35530  poimirlem3  35780  poimirlem9  35786  poimirlem16  35793  poimirlem19  35796  poimirlem30  35807  cnres2  35921  rnresequniqs  36467  diaintclN  39072  dibintclN  39181  dihintcl  39358  imaopab  40207  imaiinfv  40515  diophrw  40581  dnnumch1  40869  fnwe2lem2  40876  hbtlem6  40954  imanonrel  41201  csbima12gALTVD  42517  imassmpt  42810  limsupvaluz  43249  funcoressn  44536  fcoreslem2  44558