Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-img Structured version   Unicode version

Definition df-img 29704
Description: Define the image function. See brimg 29776 for its value. (Contributed by Scott Fenton, 12-Apr-2014.)
Assertion
Ref Expression
df-img  |- Img  =  (Image ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) )  o. Cart
)

Detailed syntax breakdown of Definition df-img
StepHypRef Expression
1 cimg 29680 . 2  class Img
2 c2nd 6716 . . . . . 6  class  2nd
3 c1st 6715 . . . . . 6  class  1st
42, 3ccom 4930 . . . . 5  class  ( 2nd 
o.  1st )
5 cvv 3047 . . . . . . 7  class  _V
65, 5cxp 4924 . . . . . 6  class  ( _V 
X.  _V )
73, 6cres 4928 . . . . 5  class  ( 1st  |`  ( _V  X.  _V ) )
84, 7cres 4928 . . . 4  class  ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) )
98cimage 29678 . . 3  class Image ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) )
10 ccart 29679 . . 3  class Cart
119, 10ccom 4930 . 2  class  (Image (
( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) )  o. Cart )
121, 11wceq 1399 1  wff Img  =  (Image ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) )  o. Cart
)
Colors of variables: wff setvar class
This definition is referenced by:  brimg  29776
  Copyright terms: Public domain W3C validator