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

Definition df-image 24405
Description: Define the image functor. This function takes a set  A to a function  x  |->  ( A
" x ), providing that the latter exists. See imageval 24469 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 24383 . 2  class Image A
3 cvv 2788 . . . 4  class  _V
43, 3cxp 4687 . . 3  class  ( _V 
X.  _V )
5 cep 4303 . . . . . 6  class  _E
63, 5ctxp 24373 . . . . 5  class  ( _V 
(x)  _E  )
71ccnv 4688 . . . . . . 7  class  `' A
85, 7ccom 4693 . . . . . 6  class  (  _E  o.  `' A )
98, 3ctxp 24373 . . . . 5  class  ( (  _E  o.  `' A
)  (x)  _V )
106, 9csymdif 24361 . . . 4  class  ( ( _V  (x)  _E  )(++) ( (  _E  o.  `' A )  (x)  _V ) )
1110crn 4690 . . 3  class  ran  (
( _V  (x)  _E  )(++) ( (  _E  o.  `' A )  (x)  _V ) )
124, 11cdif 3149 . 2  class  ( ( _V  X.  _V )  \  ran  ( ( _V 
(x)  _E  )(++) (
(  _E  o.  `' A )  (x)  _V ) ) )
132, 12wceq 1623 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  24465  funimage  24467
  Copyright terms: Public domain W3C validator