Theorem ditgex

Description: A directed integral is a set. (Contributed by Mario Carneiro, 7-Sep-2014)

	Ref	Expression
Assertion	ditgex	$$⊢{\int }_A^{B}Cdx\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-ditg	$$⊢{\int }_A^{B}Cdx=if\left(A\le B,{\int }_{\left(A,B\right)}Cdx,-{\int }_{\left(B,A\right)}Cdx\right)$$
2		itgex	$$⊢{\int }_{\left(A,B\right)}Cdx\in \mathrm{V}$$
3		negex	$$⊢-{\int }_{\left(B,A\right)}Cdx\in \mathrm{V}$$
4	2 3	ifex	$$⊢if\left(A\le B,{\int }_{\left(A,B\right)}Cdx,-{\int }_{\left(B,A\right)}Cdx\right)\in \mathrm{V}$$
5	1 4	eqeltri	$$⊢{\int }_A^{B}Cdx\in \mathrm{V}$$