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

Definition df-ima 4932
Description: Define the image of a class (as restricted by another class). Definition 6.6(2) of [TakeutiZaring] p. 24. For example, ?Error: 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> ( F " B ) = { 6 } ^ This math symbol is not active (i.e. was not declared in this scope). ( ={<.2,6>.,<.3,9>.}/\ ={1,2})->( " )={6} (ex-ima 21801). Contrast with restriction (df-res 4931) and range (df-rn 4930). For an alternate definition, see dfima2 5249. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
df-ima

Detailed syntax breakdown of Definition df-ima
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2cima 4922 . 2
41, 2cres 4921 . . 3
54crn 4920 . 2
63, 5wceq 1654 1
Colors of variables: wff set class
This definition is referenced by:  resima  5222  resima2  5223  imaeq1  5242  imaeq2  5243  dfima2  5249  nfima  5255  rnresi  5261  resiima  5262  ima0  5263  imadisj  5267  imass1  5283  imass2  5284  ndmima  5285  imaundi  5328  imaundir  5329  inimass  5332  rninxp  5354  imainrect  5356  xpima  5357  dfrn4  5375  imacnvcnv  5380  imadmres  5408  mptpreima  5409  rnco2  5423  funcnvres  5569  funimacnv  5572  fnima  5610  fores  5709  f1ores  5736  f1orescnv  5737  foimacnv  5739  resdif  5743  resfunexgALT  6006  funfvima  6021  funiunfv  6043  soisores  6095  curry1  6488  curry2  6491  fparlem3  6498  fparlem4  6499  smores2  6665  tz7.44-3  6715  tz7.49c  6752  seqomlem2  6757  seqomlem3  6758  seqomlem4  6759  sbthlem4  7269  sbthlem6  7271  sbthlem8  7273  fodomfi  7434  dffi3  7485  marypha1lem  7487  marypha2lem4  7492  dfsup3OLD  7498  ordtypelem3  7538  ordtypelem9  7544  wdomima2g  7603  rankwflemb  7768  dfac8alem  7961  dfac12lem1  8074  zorn2lem1  8427  ttukeylem3  8442  imadomg  8463  iunfo  8465  fpwwe2lem6  8561  fpwwe2lem9  8564  fpwwe2lem13  8568  gruima  8728  peano5nni  10054  1nn  10062  peano2nn  10063  seqval  11385  hashf1lem1  11755  frmdss2  14859  ghmima  15077  conjsubg  15088  gsumzaddlem  15577  gsumxp  15601  dprd2da  15651  dmdprdsplit2lem  15654  ablfac1b  15679  mplsubrglem  16553  pjdm  16985  tgrest  17274  cnconst2  17398  imacmp  17511  cmpfi  17522  conima  17539  kgencn3  17641  ptpjopn  17695  xkoccn  17702  txkgen  17735  qtoprest  17800  hmeores  17854  txflf  18089  subgntr  18187  opnsubg  18188  clsnsg  18190  tgpconcomp  18193  snclseqg  18196  tsmsf1o  18225  tsmsxplem1  18233  fmucndlem  18372  ovolicc2lem4  19467  mbflimsup  19607  itg1addlem4  19640  ellimc2  19815  c1lip3  19934  lhop  19951  dvcnvrelem1  19952  mdegfval  20036  aalioulem3  20302  taylthlem2  20341  efifo  20500  dfrelog  20514  efopnlem2  20599  xrlimcnp  20858  fsumdvdsmul  21031  dchrghm  21091  usgrares1  21475  cusgrares  21532  ex-ima  21801  subgornss  21945  efghgrp  22012  imadifxp  24086  mbfmcst  24658  ffsrn  24726  0rrv  24813  cvmliftmolem1  25072  cvmlift2lem9a  25094  cvmlift2lem9  25102  rdgprc  25526  dfrdg2  25527  dfon4  25842  ivthALT  26449  cnres2  26583  imaiinfv  26921  diophrw  26998  dnnumch1  27298  fnwe2lem2  27305  lindsmm  27454  hbtlem6  27489  funcoressn  28146  hashimarn  28350  csbima12gALTOLD  29176  csbima12gALTVD  29250  diaintclN  32096  dibintclN  32205  dihintcl  32382
  Copyright terms: Public domain W3C validator