MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ima Structured version   Visualization version   GIF version

Definition df-ima 5271
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 27602). Contrast with restriction (df-res 5270) and range (df-rn 5269). For an alternate definition, see dfima2 5618. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
df-ima (𝐴𝐵) = ran (𝐴𝐵)

Detailed syntax breakdown of Definition df-ima
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2cima 5261 . 2 class (𝐴𝐵)
41, 2cres 5260 . . 3 class (𝐴𝐵)
54crn 5259 . 2 class ran (𝐴𝐵)
63, 5wceq 1624 1 wff (𝐴𝐵) = ran (𝐴𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  resima  5581  resima2  5582  resima2OLD  5583  imaeq1  5611  imaeq2  5612  dfima2  5618  nfima  5624  rnresi  5629  resiima  5630  ima0  5631  imadisj  5634  imass1  5650  imass2  5651  imaundi  5695  imaundir  5696  inimass  5699  rninxp  5723  imainrect  5725  xpima  5726  dfrn4  5745  imacnvcnv  5749  imadmres  5780  mptpreima  5781  rnco2  5795  funcnvres  6120  funimacnv  6123  fnima  6163  fores  6277  f1ores  6304  f1orescnv  6305  foimacnv  6307  resdif  6310  fvrnressn  6583  funfvima  6647  funiunfv  6661  soisores  6732  resfunexgALT  7286  curry1  7429  curry2  7432  fparlem3  7439  fparlem4  7440  smores2  7612  tz7.44-3  7665  tz7.49c  7702  seqomlem2  7707  seqomlem3  7708  seqomlem4  7709  sbthlem4  8230  sbthlem6  8232  sbthlem8  8234  fodomfi  8396  dffi3  8494  marypha1lem  8496  marypha2lem4  8501  ordtypelem3  8582  ordtypelem9  8588  wdomima2g  8648  rankwflemb  8821  dfac8alem  9034  dfac12lem1  9149  zorn2lem1  9502  ttukeylem3  9517  imadomg  9540  iunfo  9545  fpwwe2lem6  9641  fpwwe2lem9  9644  fpwwe2lem13  9648  gruima  9808  peano5nni  11207  1nn  11215  peano2nn  11216  seqval  12998  hashimarn  13411  hashf1lem1  13423  frmdss2  17593  ghmima  17874  conjsubg  17885  gsumzaddlem  18513  gsumxp  18567  dprd2da  18633  dmdprdsplit2lem  18636  ablfac1b  18661  mplsubrglem  19633  pjdm  20245  lindsmm  20361  tgrest  21157  cnconst2  21281  imacmp  21394  cmpfi  21405  connima  21422  kgencn3  21555  ptpjopn  21609  xkoccn  21616  txkgen  21649  qtoprest  21714  hmeores  21768  txflf  22003  subgntr  22103  opnsubg  22104  clsnsg  22106  tgpconncomp  22109  snclseqg  22112  tsmsf1o  22141  tsmsxplem1  22149  fmucndlem  22288  ovolicc2lem4  23480  mbflimsup  23624  itg1addlem4  23657  ellimc2  23832  c1lip3  23953  lhop  23970  dvcnvrelem1  23971  mdegfval  24013  aalioulem3  24280  taylthlem2  24319  efifo  24484  dfrelog  24503  efopnlem2  24594  xrlimcnp  24886  fsumdvdsmul  25112  dchrghm  25172  uhgrspan1  26386  upgrreslem  26387  umgrreslem  26388  ex-ima  27602  imadifxp  29713  fresf1o  29734  elimampt  29739  imafi2  29790  ffsrn  29805  mbfmcst  30622  0rrv  30814  cvmliftmolem1  31562  cvmlift2lem9a  31584  cvmlift2lem9  31592  mrsubff1o  31711  msubff1o  31753  rdgprc  31997  dfrdg2  31998  madeval  32233  dfon4  32298  ivthALT  32628  mptsnunlem  33488  dissneqlem  33490  icoreelrnab  33505  icoreunrn  33510  poimirlem3  33717  poimirlem9  33723  poimirlem16  33730  poimirlem19  33733  poimirlem30  33744  cnres2  33867  rnresequniqs  34418  diaintclN  36841  dibintclN  36950  dihintcl  37127  imaiinfv  37750  diophrw  37816  dnnumch1  38108  fnwe2lem2  38115  hbtlem6  38193  imanonrel  38393  rp-imass  38559  csbima12gALTVD  39624  mptima  39928  imassmpt  39972  limsupvaluz  40435  funcoressn  41705
  Copyright terms: Public domain W3C validator