Theorem eliccxr 13457

Description: A member of a closed interval is an extended real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Assertion

Ref	Expression
eliccxr	⊢ (𝐴 ∈ (𝐵[,]𝐶) → 𝐴 ∈ ℝ*)

Proof of Theorem eliccxr

Step	Hyp	Ref	Expression
1		iccssxr 13452	. 2 ⊢ (𝐵[,]𝐶) ⊆ ℝ*
2	1	sseli 3959	1 ⊢ (𝐴 ∈ (𝐵[,]𝐶) → 𝐴 ∈ ℝ*)

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7413  ℝ^*cxr 11276  [,]cicc 13372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pr 5412  ax-un 7737  ax-cnex 11193  ax-resscn 11194

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-iun 4973  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-fv 6549  df-ov 7416  df-oprab 7417  df-mpo 7418  df-1st 7996  df-2nd 7997  df-xr 11281  df-icc 13376

This theorem is referenced by:  xrge0neqmnf  13474  xrge0nre  13475  isxmet2d  24282  stdbdxmet  24472  metds0  24808  metdstri  24809  metdsre  24811  metdseq0  24812  metdscnlem  24813  metnrmlem1a  24816  metnrmlem1  24817  oprpiece1res1  24918  xrge0infss  32701  xrge0mulgnn0  32959  xrge0omnd  33027  esumcvgre  34051  mblfinlem1  37623  iccintsng  45493  icoiccdif  45494  eliccnelico  45499  eliccelicod  45500  ge0xrre  45501  iblspltprt  45945  iblcncfioo  45950  itgspltprt  45951  gsumge0cl  46343  sge0tsms  46352