Theorem eliccxr 13396

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 13391	. 2 ⊢ (𝐵[,]𝐶) ⊆ ℝ*
2	1	sseli 3942	1 ⊢ (𝐴 ∈ (𝐵[,]𝐶) → 𝐴 ∈ ℝ*)

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7387  ℝ^*cxr 11207  [,]cicc 13309

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-cnex 11124  ax-resscn 11125

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-1st 7968  df-2nd 7969  df-xr 11212  df-icc 13313

This theorem is referenced by:  xrge0neqmnf  13413  xrge0nre  13414  isxmet2d  24215  stdbdxmet  24403  metds0  24739  metdstri  24740  metdsre  24742  metdseq0  24743  metdscnlem  24744  metnrmlem1a  24747  metnrmlem1  24748  oprpiece1res1  24849  xrge0infss  32683  xrge0mulgnn0  32956  xrge0omnd  33025  esumcvgre  34081  mblfinlem1  37651  iccintsng  45521  icoiccdif  45522  eliccnelico  45527  eliccelicod  45528  ge0xrre  45529  iblspltprt  45971  iblcncfioo  45976  itgspltprt  45977  gsumge0cl  46369  sge0tsms  46378