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

Definition df-image 29741
Description: Define the image functor. This function takes a set  A to a function  x  |->  ( A
" x ), providing that the latter exists. See imageval 29808 for the derivation. (Contributed by Scott Fenton, 27-Mar-2014.)
Assertion
Ref Expression
df-image  |- Image A  =  ( ( _V  X.  _V )  \  ran  (
( _V  (x)  _E  )  /_\  ( (  _E  o.  `' A ) 
(x)  _V ) ) )

Detailed syntax breakdown of Definition df-image
StepHypRef Expression
1 cA . . 3  class  A
21cimage 29717 . 2  class Image A
3 cvv 3106 . . . 4  class  _V
43, 3cxp 4986 . . 3  class  ( _V 
X.  _V )
5 cep 4778 . . . . . 6  class  _E
63, 5ctxp 29707 . . . . 5  class  ( _V 
(x)  _E  )
71ccnv 4987 . . . . . . 7  class  `' A
85, 7ccom 4992 . . . . . 6  class  (  _E  o.  `' A )
98, 3ctxp 29707 . . . . 5  class  ( (  _E  o.  `' A
)  (x)  _V )
106, 9csymdif 3714 . . . 4  class  ( ( _V  (x)  _E  )  /_\  ( (  _E  o.  `' A )  (x)  _V ) )
1110crn 4989 . . 3  class  ran  (
( _V  (x)  _E  )  /_\  ( (  _E  o.  `' A ) 
(x)  _V ) )
124, 11cdif 3458 . 2  class  ( ( _V  X.  _V )  \  ran  ( ( _V 
(x)  _E  )  /_\  ( (  _E  o.  `' A
)  (x)  _V )
) )
132, 12wceq 1398 1  wff Image A  =  ( ( _V  X.  _V )  \  ran  (
( _V  (x)  _E  )  /_\  ( (  _E  o.  `' A ) 
(x)  _V ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  brimage  29804  funimage  29806
  Copyright terms: Public domain W3C validator