Definition df-ima 5690

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 29726). Contrast with restriction (df-res 5689) and range (df-rn 5688). For an alternate definition, see dfima2 6062. (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 5680	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5679	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5678	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1542	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  6016  resima2  6017  imaeq1  6055  imaeq2  6056  dfima2  6062  nfima  6068  mptima  6072  rnresi  6075  resiima  6076  ima0  6077  imadisj  6080  imass1  6101  imass2  6102  imaundi  6150  imaundir  6151  inimass  6155  rninxp  6179  imainrect  6181  xpima  6182  dfrn4  6202  imacnvcnv  6206  imadmres  6234  mptpreima  6238  rnco2  6253  resssxp  6270  funcnvres  6627  funimacnv  6630  fnima  6681  fores  6816  f1ores  6848  f1orescnv  6849  foimacnv  6851  resdif  6855  rescnvimafod  7076  fvrnressn  7159  funfvima  7232  funiunfv  7247  soisores  7324  resfunexgALT  7934  curry1  8090  curry2  8093  fparlem3  8100  fparlem4  8101  fsplitfpar  8104  smores2  8354  tz7.44-3  8408  tz7.49c  8446  seqomlem2  8451  seqomlem3  8452  seqomlem4  8453  sbthlem4  9086  sbthlem6  9088  sbthlem8  9090  pwfir  9176  fodomfi  9325  dffi3  9426  marypha1lem  9428  marypha2lem4  9433  ordtypelem3  9515  ordtypelem9  9521  wdomima2g  9581  rankwflemb  9788  dfac8alem  10024  dfac12lem1  10138  zorn2lem1  10491  ttukeylem3  10506  imadomg  10529  iunfo  10534  fpwwe2lem5  10630  fpwwe2lem8  10633  fpwwe2lem12  10637  gruima  10797  peano5nni  12215  1nn  12223  peano2nn  12224  seqval  13977  hashimarn  14400  hashf1lem1  14415  hashf1lem1OLD  14416  frmdss2  18744  ghmima  19113  conjsubg  19124  gsumzaddlem  19789  gsumxp  19844  dprd2da  19912  dmdprdsplit2lem  19915  ablfac1b  19940  rnrhmsubrg  20352  imadrhmcl  20413  pjdm  21262  lindsmm  21383  mplsubrglem  21563  tgrest  22663  cnconst2  22787  imacmp  22901  cmpfi  22912  connima  22929  kgencn3  23062  ptpjopn  23116  xkoccn  23123  txkgen  23156  qtoprest  23221  hmeores  23275  txflf  23510  subgntr  23611  opnsubg  23612  clsnsg  23614  tgpconncomp  23617  snclseqg  23620  tsmsf1o  23649  tsmsxplem1  23657  fmucndlem  23796  ovolicc2lem4  25037  mbflimsup  25183  itg1addlem4  25216  itg1addlem4OLD  25217  ellimc2  25394  c1lip3  25516  lhop  25533  dvcnvrelem1  25534  mdegfval  25580  aalioulem3  25847  taylthlem2  25886  efifo  26056  dfrelog  26074  efopnlem2  26165  xrlimcnp  26473  fsumdvdsmul  26699  dchrghm  26759  madeval  27348  peano5n0s  27699  0n0s  27703  peano2n0s  27704  uhgrspan1  28591  upgrreslem  28592  umgrreslem  28593  ex-ima  29726  imadifxp  31863  fresf1o  31886  elimampt  31893  imafi2  31967  ffsrn  31985  pfxrn3  32138  gsumzresunsn  32237  gsumhashmul  32239  cycpmconjvlem  32331  tocyccntz  32334  qusima  32550  lmimdim  32720  dimkerim  32743  mbfmcst  33289  0rrv  33481  cvmliftmolem1  34303  cvmlift2lem9a  34325  cvmlift2lem9  34333  mrsubff1o  34537  msubff1o  34579  rdgprc  34797  dfrdg2  34798  dfon4  34896  ivthALT  35268  mptsnunlem  36267  dissneqlem  36269  icoreelrnab  36283  icoreunrn  36288  poimirlem3  36539  poimirlem9  36545  poimirlem16  36552  poimirlem19  36555  poimirlem30  36566  cnres2  36679  rnresequniqs  37249  diaintclN  39977  dibintclN  40086  dihintcl  40263  imaopab  41098  imaiinfv  41479  diophrw  41545  dnnumch1  41834  fnwe2lem2  41841  hbtlem6  41919  imanonrel  42392  csbima12gALTVD  43706  imassmpt  44015  limsupvaluz  44472  funcoressn  45800  fcoreslem2  45822