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

Definition df-ima 4864
Description: Define the image of a class (as restricted by another class). Definition 6.6(2) of [TakeutiZaring] p. 24. For example,  ( F  =  { <. 2 ,  6
>. ,  <. 3 ,  9 >. }  /\  B  =  { 1 ,  2 } )  ->  ( F
" B )  =  { 6 } (ex-ima 25884). Contrast with restriction (df-res 4863) and range (df-rn 4862). For an alternate definition, see dfima2 5187. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
df-ima  |-  ( A
" B )  =  ran  ( A  |`  B )

Detailed syntax breakdown of Definition df-ima
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2cima 4854 . 2  class  ( A
" B )
41, 2cres 4853 . . 3  class  ( A  |`  B )
54crn 4852 . 2  class  ran  ( A  |`  B )
63, 5wceq 1438 1  wff  ( A
" B )  =  ran  ( A  |`  B )
Colors of variables: wff setvar class
This definition is referenced by:  resima  5154  resima2  5155  imaeq1  5180  imaeq2  5181  dfima2  5187  nfima  5193  rnresi  5198  resiima  5199  ima0  5200  imadisj  5204  imass1  5220  imass2  5221  ndmimaOLD  5223  imaundi  5265  imaundir  5266  inimass  5269  rninxp  5293  imainrect  5295  xpima  5296  dfrn4  5313  imacnvcnv  5317  imadmres  5344  mptpreima  5345  rnco2  5359  funcnvres  5668  funimacnv  5671  fnima  5710  fores  5817  f1ores  5843  f1orescnv  5844  foimacnv  5846  resdif  5849  fvrnressn  6092  funfvima  6153  funiunfv  6166  soisores  6231  resfunexgALT  6768  curry1  6897  curry2  6900  fparlem3  6907  fparlem4  6908  smores2  7079  tz7.44-3  7132  tz7.49c  7169  seqomlem2  7174  seqomlem3  7175  seqomlem4  7176  sbthlem4  7689  sbthlem6  7691  sbthlem8  7693  fodomfi  7854  dffi3  7949  marypha1lem  7951  marypha2lem4  7956  ordtypelem3  8039  ordtypelem9  8045  wdomima2g  8105  rankwflemb  8267  dfac8alem  8462  dfac12lem1  8575  zorn2lem1  8928  ttukeylem3  8943  imadomg  8964  iunfo  8966  fpwwe2lem6  9062  fpwwe2lem9  9065  fpwwe2lem13  9069  gruima  9229  peano5nni  10614  1nn  10622  peano2nn  10623  seqval  12225  hashimarn  12609  hashf1lem1  12617  frmdss2  16640  ghmima  16896  conjsubg  16907  gsumzaddlem  17547  gsumxp  17601  dprd2da  17668  dmdprdsplit2lem  17671  ablfac1b  17696  mplsubrglem  18656  pjdm  19262  lindsmm  19378  tgrest  20167  cnconst2  20291  imacmp  20404  cmpfi  20415  conima  20432  kgencn3  20565  ptpjopn  20619  xkoccn  20626  txkgen  20659  qtoprest  20724  hmeores  20778  txflf  21013  subgntr  21113  opnsubg  21114  clsnsg  21116  tgpconcomp  21119  snclseqg  21122  tsmsf1o  21151  tsmsxplem1  21159  fmucndlem  21298  ovolicc2lem4OLD  22465  ovolicc2lem4  22466  mbflimsup  22615  mbflimsupOLD  22616  itg1addlem4  22649  ellimc2  22824  c1lip3  22943  lhop  22960  dvcnvrelem1  22961  mdegfval  23003  aalioulem3  23282  taylthlem2  23321  efifo  23488  dfrelog  23507  efopnlem2  23594  xrlimcnp  23886  fsumdvdsmul  24116  dchrghm  24176  usgrares1  25130  cusgrares  25192  ex-ima  25884  subgornss  26026  efghgrpOLD  26093  imadifxp  28208  fresf1o  28227  imafi2  28288  ffsrn  28314  mbfmcst  29083  0rrv  29286  cvmliftmolem1  30006  cvmlift2lem9a  30028  cvmlift2lem9  30036  mrsubff1o  30155  msubff1o  30197  rdgprc  30442  dfrdg2  30443  dfon4  30659  ivthALT  30990  mptsnunlem  31698  dissneqlem  31700  icoreelrnab  31715  icoreunrn  31720  poimirlem3  31901  poimirlem9  31907  poimirlem16  31914  poimirlem19  31917  poimirlem30  31928  cnres2  32053  diaintclN  34589  dibintclN  34698  dihintcl  34875  imaiinfv  35498  diophrw  35564  dnnumch1  35866  fnwe2lem2  35873  hbtlem6  35952  rp-imass  36268  csbima12gALTOLD  37123  csbima12gALTVD  37199  funcoressn  38385
  Copyright terms: Public domain W3C validator