Theorem ditgex

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

	Ref	Expression
Assertion	ditgex	|- S_ [ A -> B ] C _d x e. _V

Proof

Step	Hyp	Ref	Expression
1		df-ditg	|- S_ [ A -> B ] C _d x = if ( A <_ B , S. ( A (,) B ) C _d x , -u S. ( B (,) A ) C _d x )
2		itgex	|- S. ( A (,) B ) C _d x e. _V
3		negex	|- -u S. ( B (,) A ) C _d x e. _V
4	2 3	ifex	|- if ( A <_ B , S. ( A (,) B ) C _d x , -u S. ( B (,) A ) C _d x ) e. _V
5	1 4	eqeltri	|- S_ [ A -> B ] C _d x e. _V