Theorem iccval

Description: Value of the closed interval function. (Contributed by NM, 24-Dec-2006) (Revised by Mario Carneiro, 3-Nov-2013)

	Ref	Expression
Assertion	iccval	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 [,] 𝐵 ) = { 𝑥 ∈ ℝ* ∣ ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) } )

Proof

Step	Hyp	Ref	Expression
1		df-icc	⊢ [,] = ( 𝑦 ∈ ℝ* , 𝑧 ∈ ℝ* ↦ { 𝑥 ∈ ℝ* ∣ ( 𝑦 ≤ 𝑥 ∧ 𝑥 ≤ 𝑧 ) } )
2	1	ixxval	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 [,] 𝐵 ) = { 𝑥 ∈ ℝ* ∣ ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) } )