Theorem elicc2i

Description: Inference for membership in a closed interval. (Contributed by Scott Fenton, 3-Jun-2013)

	Ref	Expression
Hypotheses	elicc2i.1	|- A e. RR
	elicc2i.2	|- B e. RR
Assertion	elicc2i	|- ( C e. ( A [,] B ) <-> ( C e. RR /\ A <_ C /\ C <_ B ) )

Proof

Step	Hyp	Ref	Expression
1		elicc2i.1	|- A e. RR
2		elicc2i.2	|- B e. RR
3		elicc2	|- ( ( A e. RR /\ B e. RR ) -> ( C e. ( A [,] B ) <-> ( C e. RR /\ A <_ C /\ C <_ B ) ) )
4	1 2 3	mp2an	|- ( C e. ( A [,] B ) <-> ( C e. RR /\ A <_ C /\ C <_ B ) )