Definition df-ima 5636

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 30404). Contrast with restriction (df-res 5635) and range (df-rn 5634). For an alternate definition, see dfima2 6017. (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 5626	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5625	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5624	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1540	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  5970  resima2  5971  elimampt  5998  imaeq1  6010  imaeq2  6011  dfima2  6017  nfima  6023  mptima  6027  rnresi  6030  resiima  6031  ima0  6032  imadisj  6035  imass1  6056  imass2  6057  imaundi  6102  imaundir  6103  imadifssran  6104  inimass  6108  rninxp  6132  imainrect  6134  xpima  6135  dfrn4  6155  imacnvcnv  6159  imadmres  6187  mptpreima  6191  rnco2  6206  resssxp  6222  funcnvres  6564  funimacnv  6567  f1imadifssran  6572  fnima  6616  fores  6750  f1ores  6782  f1orescnv  6783  foimacnv  6785  resdif  6789  rescnvimafod  7011  fvrnressn  7099  funfvima  7170  funiunfv  7188  soisores  7268  elimampo  7490  resfunexgALT  7890  curry1  8044  curry2  8047  fparlem3  8054  fparlem4  8055  fsplitfpar  8058  smores2  8284  tz7.44-3  8337  tz7.49c  8375  seqomlem2  8380  seqomlem3  8381  seqomlem4  8382  sbthlem4  9014  sbthlem6  9016  sbthlem8  9018  fodomfi  9219  pwfir  9224  fodomfiOLD  9239  dffi3  9340  marypha1lem  9342  marypha2lem4  9347  ordtypelem3  9431  ordtypelem9  9437  wdomima2g  9497  rankwflemb  9708  dfac8alem  9942  dfac12lem1  10057  zorn2lem1  10409  ttukeylem3  10424  imadomg  10447  iunfo  10452  fpwwe2lem5  10548  fpwwe2lem8  10551  fpwwe2lem12  10555  gruima  10715  peano5nni  12149  1nn  12157  peano2nn  12158  seqval  13937  hashimarn  14365  hashf1lem1  14380  frmdss2  18755  ghmima  19134  conjsubg  19147  gsumzaddlem  19818  gsumxp  19873  dprd2da  19941  dmdprdsplit2lem  19944  ablfac1b  19969  imadrhmcl  20700  pjdm  21632  lindsmm  21753  mplsubrglem  21929  tgrest  23062  cnconst2  23186  imacmp  23300  cmpfi  23311  connima  23328  kgencn3  23461  ptpjopn  23515  xkoccn  23522  txkgen  23555  qtoprest  23620  hmeores  23674  txflf  23909  subgntr  24010  opnsubg  24011  clsnsg  24013  tgpconncomp  24016  snclseqg  24019  tsmsf1o  24048  tsmsxplem1  24056  fmucndlem  24194  ovolicc2lem4  25437  mbflimsup  25583  itg1addlem4  25616  ellimc2  25794  c1lip3  25920  lhop  25937  dvcnvrelem1  25938  mdegfval  25983  aalioulem3  26258  taylthlem2  26298  taylthlem2OLD  26299  efifo  26472  dfrelog  26490  efopnlem2  26582  xrlimcnp  26894  fsumdvdsmul  27121  fsumdvdsmulOLD  27123  dchrghm  27183  madeval  27780  seqsval  28205  noseq0  28207  noseqp1  28208  noseqind  28209  om2noseqfo  28215  dfnns2  28284  uhgrspan1  29266  upgrreslem  29267  umgrreslem  29268  ex-ima  30404  imadifxp  32563  fresf1o  32588  imafi2  32668  ffsrn  32685  pfxrn3  32895  gsumzresunsn  33022  gsumhashmul  33027  cycpmconjvlem  33096  tocyccntz  33099  qusima  33355  lmimdim  33575  dimkerim  33599  mbfmcst  34226  0rrv  34418  onvf1odlem3  35077  cvmliftmolem1  35253  cvmlift2lem9a  35275  cvmlift2lem9  35283  mrsubff1o  35487  msubff1o  35529  rdgprc  35767  dfrdg2  35768  dfon4  35866  ivthALT  36308  mptsnunlem  37311  dissneqlem  37313  icoreelrnab  37327  icoreunrn  37332  poimirlem3  37602  poimirlem9  37608  poimirlem16  37615  poimirlem19  37618  poimirlem30  37629  cnres2  37742  rnresequniqs  38301  diaintclN  41037  dibintclN  41146  dihintcl  41323  imadomfi  41975  aks6d1c2  42103  aks6d1c6lem3  42145  imaopab  42204  imaiinfv  42666  diophrw  42732  dnnumch1  43017  fnwe2lem2  43024  hbtlem6  43102  imanonrel  43566  csbima12gALTVD  44870  orbitinit  44930  orbitcl  44931  imassmpt  45240  limsupvaluz  45690  funcoressn  47027  fcoreslem2  47049