Definition df-ima 5540

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 28331). Contrast with restriction (df-res 5539) and range (df-rn 5538). For an alternate definition, see dfima2 5907. (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 5530	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5529	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5528	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1538	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  5861  resima2  5862  imaeq1  5900  imaeq2  5901  dfima2  5907  nfima  5913  mptima  5917  rnresi  5919  resiima  5920  ima0  5921  imadisj  5924  imass1  5940  imass2  5941  imaundi  5984  imaundir  5985  inimass  5988  rninxp  6012  imainrect  6014  xpima  6015  dfrn4  6035  imacnvcnv  6039  imadmres  6067  mptpreima  6071  rnco2  6087  resssxp  6103  funcnvres  6417  funimacnv  6420  fnima  6465  fores  6590  f1ores  6620  f1orescnv  6621  foimacnv  6623  resdif  6626  fvrnressn  6919  funfvima  6989  funiunfv  7004  soisores  7079  resfunexgALT  7658  curry1  7809  curry2  7812  fparlem3  7819  fparlem4  7820  fsplitfpar  7824  smores2  8006  tz7.44-3  8059  tz7.49c  8097  seqomlem2  8102  seqomlem3  8103  seqomlem4  8104  sbthlem4  8657  sbthlem6  8659  sbthlem8  8661  pwfir  8749  fodomfi  8835  dffi3  8933  marypha1lem  8935  marypha2lem4  8940  ordtypelem3  9022  ordtypelem9  9028  wdomima2g  9088  rankwflemb  9260  dfac8alem  9494  dfac12lem1  9608  zorn2lem1  9961  ttukeylem3  9976  imadomg  9999  iunfo  10004  fpwwe2lem5  10100  fpwwe2lem8  10103  fpwwe2lem12  10107  gruima  10267  peano5nni  11682  1nn  11690  peano2nn  11691  seqval  13434  hashimarn  13856  hashf1lem1  13869  hashf1lem1OLD  13870  frmdss2  18099  ghmima  18451  conjsubg  18462  gsumzaddlem  19114  gsumxp  19169  dprd2da  19237  dmdprdsplit2lem  19240  ablfac1b  19265  rnrhmsubrg  19640  pjdm  20477  lindsmm  20598  mplsubrglem  20774  tgrest  21864  cnconst2  21988  imacmp  22102  cmpfi  22113  connima  22130  kgencn3  22263  ptpjopn  22317  xkoccn  22324  txkgen  22357  qtoprest  22422  hmeores  22476  txflf  22711  subgntr  22812  opnsubg  22813  clsnsg  22815  tgpconncomp  22818  snclseqg  22821  tsmsf1o  22850  tsmsxplem1  22858  fmucndlem  22997  ovolicc2lem4  24225  mbflimsup  24371  itg1addlem4  24404  ellimc2  24581  c1lip3  24703  lhop  24720  dvcnvrelem1  24721  mdegfval  24767  aalioulem3  25034  taylthlem2  25073  efifo  25243  dfrelog  25261  efopnlem2  25352  xrlimcnp  25658  fsumdvdsmul  25884  dchrghm  25944  uhgrspan1  27197  upgrreslem  27198  umgrreslem  27199  ex-ima  28331  imadifxp  30467  fresf1o  30493  elimampt  30500  imafi2  30574  ffsrn  30592  pfxrn3  30743  gsumzresunsn  30844  gsumhashmul  30846  cycpmconjvlem  30938  tocyccntz  30941  qusima  31119  dimkerim  31233  mbfmcst  31749  0rrv  31941  cvmliftmolem1  32763  cvmlift2lem9a  32785  cvmlift2lem9  32793  mrsubff1o  32997  msubff1o  33039  rdgprc  33290  dfrdg2  33291  madeval  33622  dfon4  33770  ivthALT  34099  mptsnunlem  35061  dissneqlem  35063  icoreelrnab  35077  icoreunrn  35082  poimirlem3  35366  poimirlem9  35372  poimirlem16  35379  poimirlem19  35382  poimirlem30  35393  cnres2  35507  rnresequniqs  36055  diaintclN  38660  dibintclN  38769  dihintcl  38946  imaopab  39742  imaiinfv  40035  diophrw  40101  dnnumch1  40389  fnwe2lem2  40396  hbtlem6  40474  imanonrel  40694  csbima12gALTVD  42004  imassmpt  42298  limsupvaluz  42744  funcoressn  44028