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 5566
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 28135). Contrast with restriction (df-res 5565) and range (df-rn 5564). For an alternate definition, see dfima2 5928. (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 5556 . 2 class (𝐴𝐵)
41, 2cres 5555 . . 3 class (𝐴𝐵)
54crn 5554 . 2 class ran (𝐴𝐵)
63, 5wceq 1530 1 wff (𝐴𝐵) = ran (𝐴𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  resima  5885  resima2  5886  imaeq1  5921  imaeq2  5922  dfima2  5928  nfima  5934  mptima  5938  rnresi  5940  resiima  5941  ima0  5942  imadisj  5945  imass1  5961  imass2  5962  imaundi  6005  imaundir  6006  inimass  6009  rninxp  6033  imainrect  6035  xpima  6036  dfrn4  6056  imacnvcnv  6060  imadmres  6088  mptpreima  6089  rnco2  6103  funcnvres  6428  funimacnv  6431  fnima  6474  fores  6596  f1ores  6625  f1orescnv  6626  foimacnv  6628  resdif  6631  fvrnressn  6918  funfvima  6990  funiunfv  7004  soisores  7075  resfunexgALT  7643  curry1  7793  curry2  7796  fparlem3  7803  fparlem4  7804  fsplitfpar  7808  smores2  7985  tz7.44-3  8038  tz7.49c  8076  seqomlem2  8081  seqomlem3  8082  seqomlem4  8083  sbthlem4  8622  sbthlem6  8624  sbthlem8  8626  fodomfi  8789  dffi3  8887  marypha1lem  8889  marypha2lem4  8894  ordtypelem3  8976  ordtypelem9  8982  wdomima2g  9042  rankwflemb  9214  dfac8alem  9447  dfac12lem1  9561  zorn2lem1  9910  ttukeylem3  9925  imadomg  9948  iunfo  9953  fpwwe2lem6  10049  fpwwe2lem9  10052  fpwwe2lem13  10056  gruima  10216  peano5nni  11633  1nn  11641  peano2nn  11642  seqval  13373  hashimarn  13794  hashf1lem1  13806  frmdss2  18013  ghmima  18311  conjsubg  18322  gsumzaddlem  18963  gsumxp  19018  dprd2da  19086  dmdprdsplit2lem  19089  ablfac1b  19114  rnrhmsubrg  19489  mplsubrglem  20140  pjdm  20767  lindsmm  20888  tgrest  21683  cnconst2  21807  imacmp  21921  cmpfi  21932  connima  21949  kgencn3  22082  ptpjopn  22136  xkoccn  22143  txkgen  22176  qtoprest  22241  hmeores  22295  txflf  22530  subgntr  22630  opnsubg  22631  clsnsg  22633  tgpconncomp  22636  snclseqg  22639  tsmsf1o  22668  tsmsxplem1  22676  fmucndlem  22815  ovolicc2lem4  24036  mbflimsup  24182  itg1addlem4  24215  ellimc2  24390  c1lip3  24511  lhop  24528  dvcnvrelem1  24529  mdegfval  24571  aalioulem3  24838  taylthlem2  24877  efifo  25044  dfrelog  25062  efopnlem2  25153  xrlimcnp  25460  fsumdvdsmul  25686  dchrghm  25746  uhgrspan1  26999  upgrreslem  27000  umgrreslem  27001  ex-ima  28135  imadifxp  30266  fresf1o  30291  elimampt  30298  imafi2  30360  ffsrn  30378  pfxrn3  30531  gsumzresunsn  30605  cycpmconjvlem  30697  tocyccntz  30700  dimkerim  30909  mbfmcst  31403  0rrv  31595  cvmliftmolem1  32412  cvmlift2lem9a  32434  cvmlift2lem9  32442  mrsubff1o  32646  msubff1o  32688  rdgprc  32923  dfrdg2  32924  madeval  33173  dfon4  33238  ivthALT  33567  mptsnunlem  34488  dissneqlem  34490  icoreelrnab  34504  icoreunrn  34509  poimirlem3  34762  poimirlem9  34768  poimirlem16  34775  poimirlem19  34778  poimirlem30  34789  cnres2  34909  rnresequniqs  35457  diaintclN  38061  dibintclN  38170  dihintcl  38347  imaopab  38984  imaiinfv  39151  diophrw  39217  dnnumch1  39505  fnwe2lem2  39512  hbtlem6  39590  imanonrel  39814  rp-imass  39978  csbima12gALTVD  41092  imassmpt  41398  limsupvaluz  41850  funcoressn  43139
  Copyright terms: Public domain W3C validator