This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elioc1

Description: Membership in an open-below, closed-above interval of extended reals. (Contributed by NM, 24-Dec-2006) (Revised by Mario Carneiro, 3-Nov-2013)

		Ref	Expression
	Assertion	elioc1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (C \in (A, B] \leftrightarrow (C \in ℝ^{*} \land A < C \land C \leq B))$

Proof

Step	Hyp	Ref	Expression
1		df-ioc	$⊢ (.] = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z \leq y)\})$
2	1	elixx1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (C \in (A, B] \leftrightarrow (C \in ℝ^{*} \land A < C \land C \leq B))$