Definition df-ima 5674

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 30759). Contrast with restriction (df-res 5673) and range (df-rn 5672). For an alternate definition, see dfima2 6064. (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 5664	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5663	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5662	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1568	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  6014  resima2  6015  elimampt  6045  imaeq1  6057  imaeq2  6058  dfima2  6064  nfima  6070  mptima  6074  rnresi  6077  resiima  6078  ima0  6079  imadisj  6082  imass1  6103  imass2  6104  imaundi  6147  imaundir  6148  inimass  6152  rninxp  6177  imainrect  6179  xpima  6180  dfrn4  6201  imadifssran  6202  imadifssranOLD  6203  imacnvcnv  6207  imadmres  6235  mptpreima  6239  rnco2  6255  resssxp  6271  funcnvres  6614  funimacnv  6617  fnima  6665  fores  6802  f1ores  6835  f1orescnv  6836  foimacnv  6838  resdif  6842  rescnvimafod  7068  fvrnressn  7158  funfvima  7228  funiunfv  7246  soisores  7325  elimampo  7547  resfunexgALT  7944  curry1  8098  curry2  8101  fparlem3  8108  fparlem4  8109  fsplitfpar  8112  smores2  8340  tz7.44-3  8394  tz7.49c  8432  seqomlem2  8437  seqomlem3  8438  seqomlem4  8439  sbthlem4  9077  sbthlem6  9079  sbthlem8  9081  fodomfi  9271  pwfir  9275  imafi2  9317  dffi3  9390  marypha1lem  9392  marypha2lem4  9397  ordtypelem3  9481  ordtypelem9  9487  wdomima2g  9547  rankwflemb  9764  dfac8alem  10012  dfac12lem1  10126  zorn2lem1  10479  ttukeylem3  10494  imadomg  10517  iunfo  10522  fpwwe2lem5  10619  fpwwe2lem8  10622  fpwwe2lem12  10626  gruima  10786  peano5nni  12235  1nn  12243  peano2nn  12244  seqval  14048  hashimarn  14477  hashf1lem1  14492  frmdss2  18921  ghmima  19306  conjsubg  19319  gsumzaddlem  19990  gsumxp  20045  dprd2da  20113  dmdprdsplit2lem  20116  ablfac1b  20141  imadrhmcl  20879  pjdm  21836  lindsmm  21957  mplsubrglem  22132  tgrest  23295  cnconst2  23419  imacmp  23533  cmpfi  23544  connima  23561  kgencn3  23694  ptpjopn  23748  xkoccn  23755  txkgen  23788  qtoprest  23853  hmeores  23907  txflf  24142  subgntr  24243  opnsubg  24244  clsnsg  24246  tgpconncomp  24249  snclseqg  24252  tsmsf1o  24281  tsmsxplem1  24289  fmucndlem  24426  ovolicc2lem4  25658  mbflimsup  25804  itg1addlem4  25837  ellimc2  26015  c1lip3  26137  lhop  26154  dvcnvrelem1  26155  mdegfval  26198  aalioulem3  26474  taylthlem2  26513  efifo  26688  dfrelog  26706  efopnlem2  26798  xrlimcnp  27109  fsumdvdsmul  27335  dchrghm  27396  madeval  28001  seqsval  28457  noseq0  28459  noseqp1  28460  noseqind  28461  om2noseqfo  28467  dfnns2  28541  uhgrspan1  29619  upgrreslem  29620  umgrreslem  29621  ex-ima  30759  imadifxp  32912  fresf1o  32942  ffsrn  33039  pfxrn3  33227  gsumzresunsn  33348  gsumhashmul  33353  cycpmconjvlem  33427  tocyccntz  33430  qusima  33683  lmimdim  33960  dimkerim  33983  mbfmcst  34615  0rrv  34807  onvf1odlem3  35555  cvmliftmolem1  35739  cvmlift2lem9a  35761  cvmlift2lem9  35769  mrsubff1o  35973  msubff1o  36015  rdgprc  36250  dfrdg2  36251  dfon4  36349  ivthALT  36812  mptsnunlem  37950  dissneqlem  37952  icoreelrnab  37966  icoreunrn  37971  poimirlem3  38240  poimirlem9  38246  poimirlem16  38253  poimirlem19  38256  poimirlem30  38267  cnres2  38380  rnresequniqs  38951  diaintclN  41800  dibintclN  41909  dihintcl  42086  imadomfi  42737  aks6d1c2  42865  aks6d1c6lem3  42907  imaopab  42970  imaiinfv  43394  diophrw  43460  dnnumch1  43741  fnwe2lem2  43748  hbtlem6  43826  imanonrel  44289  csbima12gALTVD  45575  orbitinit  45635  orbitcl  45636  imassmpt  45947  limsupvaluz  46392  funcoressn  47746  fcoreslem2  47768