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 5156
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 27429). Contrast with restriction (df-res 5155) and range (df-rn 5154). For an alternate definition, see dfima2 5503. (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 5146 . 2 class (𝐴𝐵)
41, 2cres 5145 . . 3 class (𝐴𝐵)
54crn 5144 . 2 class ran (𝐴𝐵)
63, 5wceq 1523 1 wff (𝐴𝐵) = ran (𝐴𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  resima  5466  resima2  5467  resima2OLD  5468  imaeq1  5496  imaeq2  5497  dfima2  5503  nfima  5509  rnresi  5514  resiima  5515  ima0  5516  imadisj  5519  imass1  5535  imass2  5536  imaundi  5580  imaundir  5581  inimass  5584  rninxp  5608  imainrect  5610  xpima  5611  dfrn4  5630  imacnvcnv  5634  imadmres  5665  mptpreima  5666  rnco2  5680  funcnvres  6005  funimacnv  6008  fnima  6048  fores  6162  f1ores  6189  f1orescnv  6190  foimacnv  6192  resdif  6195  fvrnressn  6468  funfvima  6532  funiunfv  6546  soisores  6617  resfunexgALT  7171  curry1  7314  curry2  7317  fparlem3  7324  fparlem4  7325  smores2  7496  tz7.44-3  7549  tz7.49c  7586  seqomlem2  7591  seqomlem3  7592  seqomlem4  7593  sbthlem4  8114  sbthlem6  8116  sbthlem8  8118  fodomfi  8280  dffi3  8378  marypha1lem  8380  marypha2lem4  8385  ordtypelem3  8466  ordtypelem9  8472  wdomima2g  8532  rankwflemb  8694  dfac8alem  8890  dfac12lem1  9003  zorn2lem1  9356  ttukeylem3  9371  imadomg  9394  iunfo  9399  fpwwe2lem6  9495  fpwwe2lem9  9498  fpwwe2lem13  9502  gruima  9662  peano5nni  11061  1nn  11069  peano2nn  11070  seqval  12852  hashimarn  13265  hashf1lem1  13277  frmdss2  17447  ghmima  17728  conjsubg  17739  gsumzaddlem  18367  gsumxp  18421  dprd2da  18487  dmdprdsplit2lem  18490  ablfac1b  18515  mplsubrglem  19487  pjdm  20099  lindsmm  20215  tgrest  21011  cnconst2  21135  imacmp  21248  cmpfi  21259  connima  21276  kgencn3  21409  ptpjopn  21463  xkoccn  21470  txkgen  21503  qtoprest  21568  hmeores  21622  txflf  21857  subgntr  21957  opnsubg  21958  clsnsg  21960  tgpconncomp  21963  snclseqg  21966  tsmsf1o  21995  tsmsxplem1  22003  fmucndlem  22142  ovolicc2lem4  23334  mbflimsup  23478  itg1addlem4  23511  ellimc2  23686  c1lip3  23807  lhop  23824  dvcnvrelem1  23825  mdegfval  23867  aalioulem3  24134  taylthlem2  24173  efifo  24338  dfrelog  24357  efopnlem2  24448  xrlimcnp  24740  fsumdvdsmul  24966  dchrghm  25026  uhgrspan1  26240  upgrreslem  26241  umgrreslem  26242  ex-ima  27429  imadifxp  29540  fresf1o  29561  elimampt  29566  imafi2  29617  ffsrn  29632  mbfmcst  30449  0rrv  30641  cvmliftmolem1  31389  cvmlift2lem9a  31411  cvmlift2lem9  31419  mrsubff1o  31538  msubff1o  31580  rdgprc  31824  dfrdg2  31825  madeval  32060  dfon4  32125  ivthALT  32455  mptsnunlem  33315  dissneqlem  33317  icoreelrnab  33332  icoreunrn  33337  poimirlem3  33542  poimirlem9  33548  poimirlem16  33555  poimirlem19  33558  poimirlem30  33569  cnres2  33692  rnresequniqs  34243  diaintclN  36664  dibintclN  36773  dihintcl  36950  imaiinfv  37573  diophrw  37639  dnnumch1  37931  fnwe2lem2  37938  hbtlem6  38016  imanonrel  38216  rp-imass  38382  csbima12gALTVD  39447  mptima  39751  imassmpt  39795  limsupvaluz  40258  funcoressn  41528
  Copyright terms: Public domain W3C validator