Theorem iccshftli

Description: Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Hypotheses	iccshftli.1	|- A e. RR
	iccshftli.2	|- B e. RR
	iccshftli.3	|- R e. RR
	iccshftli.4	|- ( A - R ) = C
	iccshftli.5	|- ( B - R ) = D
Assertion	iccshftli	|- ( X e. ( A [,] B ) -> ( X - R ) e. ( C [,] D ) )

Proof

Step	Hyp	Ref	Expression
1		iccshftli.1	|- A e. RR
2		iccshftli.2	|- B e. RR
3		iccshftli.3	|- R e. RR
4		iccshftli.4	|- ( A - R ) = C
5		iccshftli.5	|- ( B - R ) = D
6		iccssre	|- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
7	1 2 6	mp2an	|- ( A [,] B ) C_ RR
8	7	sseli	|- ( X e. ( A [,] B ) -> X e. RR )
9	4 5	iccshftl	|- ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ R e. RR ) ) -> ( X e. ( A [,] B ) <-> ( X - R ) e. ( C [,] D ) ) )
10	1 2 9	mpanl12	|- ( ( X e. RR /\ R e. RR ) -> ( X e. ( A [,] B ) <-> ( X - R ) e. ( C [,] D ) ) )
11	3 10	mpan2	|- ( X e. RR -> ( X e. ( A [,] B ) <-> ( X - R ) e. ( C [,] D ) ) )
12	11	biimpd	|- ( X e. RR -> ( X e. ( A [,] B ) -> ( X - R ) e. ( C [,] D ) ) )
13	8 12	mpcom	|- ( X e. ( A [,] B ) -> ( X - R ) e. ( C [,] D ) )