Definition df-ima 5638

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 30500). Contrast with restriction (df-res 5637) and range (df-rn 5636). For an alternate definition, see dfima2 6022. (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 5628	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5627	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5626	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1542	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  5975  resima2  5976  elimampt  6003  imaeq1  6015  imaeq2  6016  dfima2  6022  nfima  6028  mptima  6032  rnresi  6035  resiima  6036  ima0  6037  imadisj  6040  imass1  6061  imass2  6062  imaundi  6108  imaundir  6109  imadifssran  6110  inimass  6114  rninxp  6138  imainrect  6140  xpima  6141  dfrn4  6161  imacnvcnv  6165  imadmres  6193  mptpreima  6197  rnco2  6213  resssxp  6229  funcnvres  6571  funimacnv  6574  f1imadifssran  6579  fnima  6623  fores  6757  f1ores  6789  f1orescnv  6790  foimacnv  6792  resdif  6796  rescnvimafod  7020  fvrnressn  7108  funfvima  7178  funiunfv  7196  soisores  7275  elimampo  7497  resfunexgALT  7894  curry1  8048  curry2  8051  fparlem3  8058  fparlem4  8059  fsplitfpar  8062  smores2  8288  tz7.44-3  8341  tz7.49c  8379  seqomlem2  8384  seqomlem3  8385  seqomlem4  8386  sbthlem4  9022  sbthlem6  9024  sbthlem8  9026  fodomfi  9216  pwfir  9221  fodomfiOLD  9234  imafi2  9265  dffi3  9338  marypha1lem  9340  marypha2lem4  9345  ordtypelem3  9429  ordtypelem9  9435  wdomima2g  9495  rankwflemb  9709  dfac8alem  9943  dfac12lem1  10058  zorn2lem1  10410  ttukeylem3  10425  imadomg  10448  iunfo  10453  fpwwe2lem5  10550  fpwwe2lem8  10553  fpwwe2lem12  10557  gruima  10717  peano5nni  12152  1nn  12160  peano2nn  12161  seqval  13939  hashimarn  14367  hashf1lem1  14382  frmdss2  18792  ghmima  19170  conjsubg  19183  gsumzaddlem  19854  gsumxp  19909  dprd2da  19977  dmdprdsplit2lem  19980  ablfac1b  20005  imadrhmcl  20734  pjdm  21666  lindsmm  21787  mplsubrglem  21963  tgrest  23107  cnconst2  23231  imacmp  23345  cmpfi  23356  connima  23373  kgencn3  23506  ptpjopn  23560  xkoccn  23567  txkgen  23600  qtoprest  23665  hmeores  23719  txflf  23954  subgntr  24055  opnsubg  24056  clsnsg  24058  tgpconncomp  24061  snclseqg  24064  tsmsf1o  24093  tsmsxplem1  24101  fmucndlem  24238  ovolicc2lem4  25481  mbflimsup  25627  itg1addlem4  25660  ellimc2  25838  c1lip3  25964  lhop  25981  dvcnvrelem1  25982  mdegfval  26027  aalioulem3  26302  taylthlem2  26342  taylthlem2OLD  26343  efifo  26516  dfrelog  26534  efopnlem2  26626  xrlimcnp  26938  fsumdvdsmul  27165  fsumdvdsmulOLD  27167  dchrghm  27227  madeval  27830  seqsval  28269  noseq0  28271  noseqp1  28272  noseqind  28273  om2noseqfo  28279  dfnns2  28351  uhgrspan1  29359  upgrreslem  29360  umgrreslem  29361  ex-ima  30500  imadifxp  32658  fresf1o  32691  ffsrn  32788  pfxrn3  33004  gsumzresunsn  33126  gsumhashmul  33131  cycpmconjvlem  33204  tocyccntz  33207  qusima  33470  lmimdim  33741  dimkerim  33765  mbfmcst  34397  0rrv  34589  onvf1odlem3  35280  cvmliftmolem1  35456  cvmlift2lem9a  35478  cvmlift2lem9  35486  mrsubff1o  35690  msubff1o  35732  rdgprc  35967  dfrdg2  35968  dfon4  36066  ivthALT  36510  mptsnunlem  37514  dissneqlem  37516  icoreelrnab  37530  icoreunrn  37535  poimirlem3  37795  poimirlem9  37801  poimirlem16  37808  poimirlem19  37811  poimirlem30  37822  cnres2  37935  rnresequniqs  38506  diaintclN  41355  dibintclN  41464  dihintcl  41641  imadomfi  42293  aks6d1c2  42421  aks6d1c6lem3  42463  imaopab  42524  imaiinfv  42971  diophrw  43037  dnnumch1  43322  fnwe2lem2  43329  hbtlem6  43407  imanonrel  43870  csbima12gALTVD  45173  orbitinit  45233  orbitcl  45234  imassmpt  45542  limsupvaluz  45988  funcoressn  47324  fcoreslem2  47346