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

Definition df-image 25231
Description: Define the image functor. This function takes a set  A to a function  x  |->  ( A
" x ), providing that the latter exists. See imageval 25295 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 25209 . 2  class Image A
3 cvv 2873 . . . 4  class  _V
43, 3cxp 4790 . . 3  class  ( _V 
X.  _V )
5 cep 4406 . . . . . 6  class  _E
63, 5ctxp 25199 . . . . 5  class  ( _V 
(x)  _E  )
71ccnv 4791 . . . . . . 7  class  `' A
85, 7ccom 4796 . . . . . 6  class  (  _E  o.  `' A )
98, 3ctxp 25199 . . . . 5  class  ( (  _E  o.  `' A
)  (x)  _V )
106, 9csymdif 25187 . . . 4  class  ( ( _V  (x)  _E  )(++) ( (  _E  o.  `' A )  (x)  _V ) )
1110crn 4793 . . 3  class  ran  (
( _V  (x)  _E  )(++) ( (  _E  o.  `' A )  (x)  _V ) )
124, 11cdif 3235 . 2  class  ( ( _V  X.  _V )  \  ran  ( ( _V 
(x)  _E  )(++) (
(  _E  o.  `' A )  (x)  _V ) ) )
132, 12wceq 1647 1  wff Image A  =  ( ( _V  X.  _V )  \  ran  (
( _V  (x)  _E  )(++) ( (  _E  o.  `' A )  (x)  _V ) ) )
Colors of variables: wff set class
This definition is referenced by:  brimage  25291  funimage  25293
  Copyright terms: Public domain W3C validator