Definition df-ima 5370

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 27891). Contrast with restriction (df-res 5369) and range (df-rn 5368). For an alternate definition, see dfima2 5724. (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 5360	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5359	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5358	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1601	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  5682  resima2  5683  imaeq1  5717  imaeq2  5718  dfima2  5724  nfima  5730  rnresi  5735  resiima  5736  ima0  5737  imadisj  5740  imass1  5756  imass2  5757  imaundi  5801  imaundir  5802  inimass  5805  rninxp  5829  imainrect  5831  xpima  5832  dfrn4  5851  imacnvcnv  5855  imadmres  5883  mptpreima  5884  rnco2  5898  funcnvres  6214  funimacnv  6217  fnima  6258  fores  6378  f1ores  6407  f1orescnv  6408  foimacnv  6410  resdif  6413  fvrnressn  6696  funfvima  6766  funiunfv  6780  soisores  6851  resfunexgALT  7410  curry1  7552  curry2  7555  fparlem3  7562  fparlem4  7563  smores2  7736  tz7.44-3  7789  tz7.49c  7826  seqomlem2  7831  seqomlem3  7832  seqomlem4  7833  sbthlem4  8363  sbthlem6  8365  sbthlem8  8367  fodomfi  8529  dffi3  8627  marypha1lem  8629  marypha2lem4  8634  ordtypelem3  8716  ordtypelem9  8722  wdomima2g  8782  rankwflemb  8955  dfac8alem  9187  dfac12lem1  9302  zorn2lem1  9655  ttukeylem3  9670  imadomg  9693  iunfo  9698  fpwwe2lem6  9794  fpwwe2lem9  9797  fpwwe2lem13  9801  gruima  9961  peano5nni  11382  1nn  11392  peano2nn  11393  seqval  13135  hashimarn  13547  hashf1lem1  13559  frmdss2  17798  ghmima  18076  conjsubg  18087  gsumzaddlem  18718  gsumxp  18772  dprd2da  18839  dmdprdsplit2lem  18842  ablfac1b  18867  mplsubrglem  19847  pjdm  20461  lindsmm  20582  tgrest  21382  cnconst2  21506  imacmp  21620  cmpfi  21631  connima  21648  kgencn3  21781  ptpjopn  21835  xkoccn  21842  txkgen  21875  qtoprest  21940  hmeores  21994  txflf  22229  subgntr  22329  opnsubg  22330  clsnsg  22332  tgpconncomp  22335  snclseqg  22338  tsmsf1o  22367  tsmsxplem1  22375  fmucndlem  22514  ovolicc2lem4  23735  mbflimsup  23881  itg1addlem4  23914  ellimc2  24089  c1lip3  24210  lhop  24227  dvcnvrelem1  24228  mdegfval  24270  aalioulem3  24537  taylthlem2  24576  efifo  24742  dfrelog  24760  efopnlem2  24851  xrlimcnp  25158  fsumdvdsmul  25384  dchrghm  25444  uhgrspan1  26667  upgrreslem  26668  umgrreslem  26669  ex-ima  27891  imadifxp  29994  fresf1o  30015  elimampt  30020  imafi2  30072  ffsrn  30087  dimkerim  30449  mbfmcst  30927  0rrv  31120  cvmliftmolem1  31870  cvmlift2lem9a  31892  cvmlift2lem9  31900  mrsubff1o  32019  msubff1o  32061  rdgprc  32296  dfrdg2  32297  madeval  32532  dfon4  32597  ivthALT  32926  mptsnunlem  33788  dissneqlem  33790  icoreelrnab  33804  icoreunrn  33809  poimirlem3  34047  poimirlem9  34053  poimirlem16  34060  poimirlem19  34063  poimirlem30  34074  cnres2  34195  rnresequniqs  34739  diaintclN  37221  dibintclN  37330  dihintcl  37507  imaiinfv  38230  diophrw  38296  dnnumch1  38587  fnwe2lem2  38594  hbtlem6  38672  imanonrel  38870  rp-imass  39035  csbima12gALTVD  40080  mptima  40368  imassmpt  40406  limsupvaluz  40862  funcoressn  42120