Metamath Proof Explorer

Theorem elioo3g

Description: Membership in a set of open intervals of extended reals. We use the fact that an operation's value is empty outside of its domain to show A e. RR* and B e. RR* . (Contributed by NM, 24-Dec-2006) (Revised by Mario Carneiro, 3-Nov-2013)

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

Proof

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