Theorem itgex

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

	Ref	Expression
Assertion	itgex	$$⊢{\int }_{A}Bdx\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-itg	$$⊢{\int }_{A}Bdx=\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in A\wedge 0\le y\right),y,0\right)\right)\right)$$
2		sumex	$$⊢\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{B}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in A\wedge 0\le y\right),y,0\right)\right)\right)\in \mathrm{V}$$
3	1 2	eqeltri	$$⊢{\int }_{A}Bdx\in \mathrm{V}$$