Metamath Proof Explorer

Theorem itgex

Description: An integral is a set. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Assertion itgex 
|- S. A B _d x e. _V

Proof

Step Hyp Ref Expression
1 df-itg 
 |-  S. A B _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( B / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) )
2 sumex 
 |-  sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> [_ ( Re ` ( B / ( _i ^ k ) ) ) / y ]_ if ( ( x e. A /\ 0 <_ y ) , y , 0 ) ) ) ) e. _V
3 1 2 eqeltri 
 |-  S. A B _d x e. _V