Definition df-ima 5644

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 30512). Contrast with restriction (df-res 5643) and range (df-rn 5642). For an alternate definition, see dfima2 6028. (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 5634	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5633	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5632	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1542	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  5981  resima2  5982  elimampt  6009  imaeq1  6021  imaeq2  6022  dfima2  6028  nfima  6034  mptima  6038  rnresi  6041  resiima  6042  ima0  6043  imadisj  6046  imass1  6067  imass2  6068  imaundi  6114  imaundir  6115  imadifssran  6116  inimass  6120  rninxp  6144  imainrect  6146  xpima  6147  dfrn4  6167  imacnvcnv  6171  imadmres  6199  mptpreima  6203  rnco2  6219  resssxp  6235  funcnvres  6577  funimacnv  6580  f1imadifssran  6585  fnima  6629  fores  6763  f1ores  6795  f1orescnv  6796  foimacnv  6798  resdif  6802  rescnvimafod  7026  fvrnressn  7115  funfvima  7185  funiunfv  7203  soisores  7282  elimampo  7504  resfunexgALT  7901  curry1  8054  curry2  8057  fparlem3  8064  fparlem4  8065  fsplitfpar  8068  smores2  8294  tz7.44-3  8347  tz7.49c  8385  seqomlem2  8390  seqomlem3  8391  seqomlem4  8392  sbthlem4  9028  sbthlem6  9030  sbthlem8  9032  fodomfi  9222  pwfir  9227  fodomfiOLD  9240  imafi2  9271  dffi3  9344  marypha1lem  9346  marypha2lem4  9351  ordtypelem3  9435  ordtypelem9  9441  wdomima2g  9501  rankwflemb  9717  dfac8alem  9951  dfac12lem1  10066  zorn2lem1  10418  ttukeylem3  10433  imadomg  10456  iunfo  10461  fpwwe2lem5  10558  fpwwe2lem8  10561  fpwwe2lem12  10565  gruima  10725  peano5nni  12177  1nn  12185  peano2nn  12186  seqval  13974  hashimarn  14402  hashf1lem1  14417  frmdss2  18831  ghmima  19212  conjsubg  19225  gsumzaddlem  19896  gsumxp  19951  dprd2da  20019  dmdprdsplit2lem  20022  ablfac1b  20047  imadrhmcl  20774  pjdm  21687  lindsmm  21808  mplsubrglem  21982  tgrest  23124  cnconst2  23248  imacmp  23362  cmpfi  23373  connima  23390  kgencn3  23523  ptpjopn  23577  xkoccn  23584  txkgen  23617  qtoprest  23682  hmeores  23736  txflf  23971  subgntr  24072  opnsubg  24073  clsnsg  24075  tgpconncomp  24078  snclseqg  24081  tsmsf1o  24110  tsmsxplem1  24118  fmucndlem  24255  ovolicc2lem4  25487  mbflimsup  25633  itg1addlem4  25666  ellimc2  25844  c1lip3  25966  lhop  25983  dvcnvrelem1  25984  mdegfval  26027  aalioulem3  26300  taylthlem2  26339  efifo  26511  dfrelog  26529  efopnlem2  26621  xrlimcnp  26932  fsumdvdsmul  27158  dchrghm  27219  madeval  27824  seqsval  28280  noseq0  28282  noseqp1  28283  noseqind  28284  om2noseqfo  28290  dfnns2  28364  uhgrspan1  29372  upgrreslem  29373  umgrreslem  29374  ex-ima  30512  imadifxp  32671  fresf1o  32704  ffsrn  32801  pfxrn3  33001  gsumzresunsn  33123  gsumhashmul  33128  cycpmconjvlem  33202  tocyccntz  33205  qusima  33468  lmimdim  33748  dimkerim  33771  mbfmcst  34403  0rrv  34595  onvf1odlem3  35287  cvmliftmolem1  35463  cvmlift2lem9a  35485  cvmlift2lem9  35493  mrsubff1o  35697  msubff1o  35739  rdgprc  35974  dfrdg2  35975  dfon4  36073  ivthALT  36517  mptsnunlem  37654  dissneqlem  37656  icoreelrnab  37670  icoreunrn  37675  poimirlem3  37944  poimirlem9  37950  poimirlem16  37957  poimirlem19  37960  poimirlem30  37971  cnres2  38084  rnresequniqs  38655  diaintclN  41504  dibintclN  41613  dihintcl  41790  imadomfi  42441  aks6d1c2  42569  aks6d1c6lem3  42611  imaopab  42672  imaiinfv  43125  diophrw  43191  dnnumch1  43472  fnwe2lem2  43479  hbtlem6  43557  imanonrel  44020  csbima12gALTVD  45323  orbitinit  45383  orbitcl  45384  imassmpt  45691  limsupvaluz  46136  funcoressn  47484  fcoreslem2  47506