Theorem iccssre 13331

Description: A closed real interval is a set of reals. (Contributed by FL, 6-Jun-2007.) (Proof shortened by Paul Chapman, 21-Jan-2008.)

Assertion

Ref	Expression
iccssre	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)

Proof of Theorem iccssre

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elicc2 13313	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
2	1	biimp3a 1471	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))
3	2	simp1d 1142	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
4	3	3expia 1121	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ))
5	4	ssrdv 3936	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2113   ⊆ wss 3898   class class class wbr 5093  (class class class)co 7352  ℝcr 11012   ≤ cle 11154  [,]cicc 13250

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-cnex 11069  ax-resscn 11070  ax-pre-lttri 11087  ax-pre-lttrn 11088

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7355  df-oprab 7356  df-mpo 7357  df-er 8628  df-en 8876  df-dom 8877  df-sdom 8878  df-pnf 11155  df-mnf 11156  df-xr 11157  df-ltxr 11158  df-le 11159  df-icc 13254

This theorem is referenced by:  iccssred  13336  iccsupr  13344  iccsplit  13387  iccshftri  13389  iccshftli  13391  iccdili  13393  icccntri  13395  unitssre  13401  supicc  13403  supiccub  13404  supicclub  13405  icccld  24682  iccntr  24738  icccmplem2  24740  icccmplem3  24741  icccmp  24742  retopconn  24746  iccconn  24747  cnmpopc  24850  iihalf1cn  24854  iihalf1cnOLD  24855  iihalf2cn  24857  iihalf2cnOLD  24858  icoopnst  24864  iocopnst  24865  icchmeo  24866  icchmeoOLD  24867  xrhmeo  24872  icccvx  24876  cnheiborlem  24881  htpycc  24907  pcocn  24945  pcohtpylem  24947  pcopt  24950  pcopt2  24951  pcoass  24952  pcorevlem  24954  ivthlem2  25381  ivthlem3  25382  ivthicc  25387  evthicc  25388  ovolficcss  25398  ovolicc1  25445  ovolicc2  25451  ovolicc  25452  iccmbl  25495  ovolioo  25497  dyadss  25523  volcn  25535  volivth  25536  vitalilem2  25538  vitalilem4  25540  mbfimaicc  25560  mbfi1fseqlem4  25647  itgioo  25745  rollelem  25921  rolle  25922  cmvthOLD  25924  mvth  25925  dvlip  25926  c1liplem1  25929  c1lip1  25930  c1lip3  25932  dvgt0lem1  25935  dvgt0lem2  25936  dvgt0  25937  dvlt0  25938  dvge0  25939  dvle  25940  dvivthlem1  25941  dvivth  25943  dvne0  25944  lhop1lem  25946  dvcvx  25953  dvfsumleOLD  25955  dvfsumge  25956  dvfsumabs  25957  ftc1lem1  25970  ftc1a  25972  ftc1lem4  25974  ftc1lem5  25975  ftc1lem6  25976  ftc1  25977  ftc1cn  25978  ftc2  25979  ftc2ditglem  25980  ftc2ditg  25981  itgparts  25982  itgsubstlem  25983  itgpowd  25985  aalioulem3  26270  reeff1olem  26384  efcvx  26387  pilem3  26391  pige3ALT  26457  sinord  26471  recosf1o  26472  resinf1o  26473  efif1olem4  26482  asinrecl  26840  acosrecl  26841  emre  26944  pntlem3  27548  ttgcontlem1  28864  signsply0  34585  iblidicc  34626  ftc2re  34632  iccsconn  35313  iccllysconn  35315  cvmliftlem10  35359  ivthALT  36400  sin2h  37670  cos2h  37671  mblfinlem2  37718  ftc1cnnclem  37751  ftc1cnnc  37752  ftc1anclem7  37759  ftc1anc  37761  ftc2nc  37762  areacirclem2  37769  areacirclem3  37770  areacirclem4  37771  areacirc  37773  iccbnd  37900  icccmpALT  37901  arearect  43332  areaquad  43333  lhe4.4ex1a  44446  lefldiveq  45417  itgsin0pilem1  46072  ibliccsinexp  46073  iblioosinexp  46075  itgsinexplem1  46076  itgsinexp  46077  iblspltprt  46095  fourierdlem5  46234  fourierdlem9  46238  fourierdlem18  46247  fourierdlem24  46253  fourierdlem62  46290  fourierdlem66  46294  fourierdlem74  46302  fourierdlem75  46303  fourierdlem83  46311  fourierdlem87  46315  fourierdlem93  46321  fourierdlem95  46323  fourierdlem102  46330  fourierdlem103  46331  fourierdlem104  46332  fourierdlem112  46340  fourierdlem114  46342  sqwvfoura  46350  sqwvfourb  46351