Theorem elioc1 13194

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.)

Assertion

Ref	Expression
elioc1	⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)))

Proof of Theorem elioc1

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ioc 13157	. 2 ⊢ (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
2	1	elixx1 13161	1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086   ∈ wcel 2105   class class class wbr 5087  (class class class)co 7315  ℝ^*cxr 11081   < clt 11082   ≤ cle 11083  (,]cioc 13153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pr 5367  ax-un 7628  ax-cnex 11000  ax-resscn 11001

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3443  df-sbc 3727  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-if 4472  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-br 5088  df-opab 5150  df-id 5507  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-iota 6417  df-fun 6467  df-fv 6473  df-ov 7318  df-oprab 7319  df-mpo 7320  df-xr 11086  df-ioc 13157

This theorem is referenced by:  ubioc1  13205  elioc2  13215  leordtvallem1  22433  pnfnei  22443  mnfnei  22444  xrge0tsms  24069  lhop1  25250  xrlimcnp  26190  iocinioc2  31208  xrge0tsmsd  31425  xrge0iifcnv  31989  lmxrge0  32008  iocinico  41247  rfcnpre4  42798  iocgtlb  43277  iocleub  43278  eliocd  43282  lenelioc  43311  eenglngeehlnmlem1  46335