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

Definition df-img 24407
Description: Define the image function. See brimg 24476 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 24385 . 2  class Img
2 c2nd 6121 . . . . . 6  class  2nd
3 c1st 6120 . . . . . 6  class  1st
42, 3ccom 4693 . . . . 5  class  ( 2nd 
o.  1st )
5 cvv 2788 . . . . . . 7  class  _V
65, 5cxp 4687 . . . . . 6  class  ( _V 
X.  _V )
73, 6cres 4691 . . . . 5  class  ( 1st  |`  ( _V  X.  _V ) )
84, 7cres 4691 . . . 4  class  ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) )
98cimage 24383 . . 3  class Image ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) )
10 ccart 24384 . . 3  class Cart
119, 10ccom 4693 . 2  class  (Image (
( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) )  o. Cart )
121, 11wceq 1623 1  wff Img  =  (Image ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) )  o. Cart
)
Colors of variables: wff set class
This definition is referenced by:  brimg  24476
  Copyright terms: Public domain W3C validator