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 25702
Description: Define the image function. See brimg 25774 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 25678 . 2  class Img
2 c2nd 6340 . . . . . 6  class  2nd
3 c1st 6339 . . . . . 6  class  1st
42, 3ccom 4874 . . . . 5  class  ( 2nd 
o.  1st )
5 cvv 2948 . . . . . . 7  class  _V
65, 5cxp 4868 . . . . . 6  class  ( _V 
X.  _V )
73, 6cres 4872 . . . . 5  class  ( 1st  |`  ( _V  X.  _V ) )
84, 7cres 4872 . . . 4  class  ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) )
98cimage 25676 . . 3  class Image ( ( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) )
10 ccart 25677 . . 3  class Cart
119, 10ccom 4874 . 2  class  (Image (
( 2nd  o.  1st )  |`  ( 1st  |`  ( _V  X.  _V ) ) )  o. Cart )
121, 11wceq 1652 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  25774
  Copyright terms: Public domain W3C validator