Definition df-ima 5679

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 30823). Contrast with restriction (df-res 5678) and range (df-rn 5677). For an alternate definition, see dfima2 6069. (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 5669	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 5668	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 5667	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1570	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is used by:  resima  6019  resima2  6020  elimampt  6050  imaeq1  6062  imaeq2  6063  dfima2  6069  nfima  6075  mptima  6079  rnresi  6082  resiima  6083  ima0  6084  imadisj  6087  imass1  6108  imass2  6109  imaundi  6152  imaundir  6153  inimass  6157  rninxp  6182  imainrect  6184  xpima  6185  dfrn4  6206  imadifssran  6207  imadifssranOLD  6208  imacnvcnv  6212  imadmres  6240  mptpreima  6244  rnco2  6260  resssxp  6277  funcnvres  6621  funimacnv  6624  fnima  6672  fores  6809  f1ores  6842  f1orescnv  6843  foimacnv  6845  resdif  6849  rescnvimafod  7075  fvrnressn  7165  funfvima  7235  funiunfv  7253  soisores  7336  elimampo  7560  resfunexgALT  7954  curry1  8108  curry2  8111  fparlem3  8118  fparlem4  8119  fsplitfpar  8122  smores2  8350  tz7.44-3  8404  tz7.49c  8442  seqomlem2  8447  seqomlem3  8448  seqomlem4  8449  sbthlem4  9088  sbthlem6  9090  sbthlem8  9092  fodomfi  9282  pwfir  9286  imafi2  9328  dffi3  9401  marypha1lem  9403  marypha2lem4  9408  ordtypelem3  9492  ordtypelem9  9498  wdomima2g  9558  rankwflemb  9775  dfac8alem  10032  dfac12lem1  10146  zorn2lem1  10498  ttukeylem3  10513  imadomg  10536  iunfo  10541  fpwwe2lem5  10638  fpwwe2lem8  10641  fpwwe2lem12  10645  gruima  10805  peano5nni  12254  1nn  12262  peano2nn  12263  seqval  14068  hashimarn  14497  hashf1lem1  14512  frmdss2  18947  ghmima  19332  conjsubg  19345  gsumzaddlem  20016  gsumxp  20071  dprd2da  20139  dmdprdsplit2lem  20142  ablfac1b  20167  imadrhmcl  20930  pjdm  21887  lindsmm  22008  mplsubrglem  22183  tgrest  23346  cnconst2  23470  imacmp  23584  cmpfi  23595  connima  23612  kgencn3  23745  ptpjopn  23799  xkoccn  23806  txkgen  23839  qtoprest  23904  hmeores  23958  txflf  24193  subgntr  24294  opnsubg  24295  clsnsg  24297  tgpconncomp  24300  snclseqg  24303  tsmsf1o  24332  tsmsxplem1  24340  fmucndlem  24477  ovolicc2lem4  25709  mbflimsup  25855  itg1addlem4  25888  ellimc2  26066  c1lip3  26188  lhop  26205  dvcnvrelem1  26206  mdegfval  26249  aalioulem3  26527  taylthlem2  26567  efifo  26742  dfrelog  26760  efopnlem2  26852  xrlimcnp  27163  fsumdvdsmul  27389  dchrghm  27450  madeval  28055  seqsval  28511  noseq0  28513  noseqp1  28514  noseqind  28515  om2noseqfo  28521  dfnns2  28595  uhgrspan1  29683  upgrreslem  29684  umgrreslem  29685  ex-ima  30823  imadifxp  32976  fresf1o  33006  ffsrn  33103  pfxrn3  33291  gsumzresunsn  33406  gsumhashmul  33411  cycpmconjvlem  33485  tocyccntz  33488  qusima  33741  lmimdim  34018  dimkerim  34041  mbfmcst  34673  0rrv  34865  onvf1odlem3  35605  cvmliftmolem1  35786  cvmlift2lem9a  35808  cvmlift2lem9  35816  mrsubff1o  36020  msubff1o  36062  rdgprc  36297  dfrdg2  36298  dfon4  36396  ivthALT  36879  mptsnunlem  38017  dissneqlem  38019  icoreelrnab  38033  icoreunrn  38038  poimirlem3  38307  poimirlem9  38313  poimirlem16  38320  poimirlem19  38323  poimirlem30  38334  cnres2  38447  rnresequniqs  39016  diaintclN  41865  dibintclN  41974  dihintcl  42151  imadomfi  42802  aks6d1c2  42930  aks6d1c6lem3  42972  imaopab  43035  imaiinfv  43457  diophrw  43523  dnnumch1  43804  fnwe2lem2  43811  hbtlem6  43889  imanonrel  44352  csbima12gALTVD  45638  orbitinit  45698  orbitcl  45699  imassmpt  46010  limsupvaluz  46455  funcoressn  47812  fcoreslem2  47834