Theorem iccssre 13357

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 13339	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
2	1	biimp3a 1472	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))
3	2	simp1d 1143	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
4	3	3expia 1122	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ))
5	4	ssrdv 3941	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   ∈ wcel 2114   ⊆ wss 3903   class class class wbr 5100  (class class class)co 7368  ℝcr 11037   ≤ cle 11179  [,]cicc 13276

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095  ax-pre-lttri 11112  ax-pre-lttrn 11113

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-po 5540  df-so 5541  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-icc 13280

This theorem is referenced by:  iccssred  13362  iccsupr  13370  iccsplit  13413  iccshftri  13415  iccshftli  13417  iccdili  13419  icccntri  13421  unitssre  13427  supicc  13429  supiccub  13430  supicclub  13431  icccld  24722  iccntr  24778  icccmplem2  24780  icccmplem3  24781  icccmp  24782  retopconn  24786  iccconn  24787  cnmpopc  24890  iihalf1cn  24894  iihalf1cnOLD  24895  iihalf2cn  24897  iihalf2cnOLD  24898  icoopnst  24904  iocopnst  24905  icchmeo  24906  icchmeoOLD  24907  xrhmeo  24912  icccvx  24916  cnheiborlem  24921  htpycc  24947  pcocn  24985  pcohtpylem  24987  pcopt  24990  pcopt2  24991  pcoass  24992  pcorevlem  24994  ivthlem2  25421  ivthlem3  25422  ivthicc  25427  evthicc  25428  ovolficcss  25438  ovolicc1  25485  ovolicc2  25491  ovolicc  25492  iccmbl  25535  ovolioo  25537  dyadss  25563  volcn  25575  volivth  25576  vitalilem2  25578  vitalilem4  25580  mbfimaicc  25600  mbfi1fseqlem4  25687  itgioo  25785  rollelem  25961  rolle  25962  cmvthOLD  25964  mvth  25965  dvlip  25966  c1liplem1  25969  c1lip1  25970  c1lip3  25972  dvgt0lem1  25975  dvgt0lem2  25976  dvgt0  25977  dvlt0  25978  dvge0  25979  dvle  25980  dvivthlem1  25981  dvivth  25983  dvne0  25984  lhop1lem  25986  dvcvx  25993  dvfsumleOLD  25995  dvfsumge  25996  dvfsumabs  25997  ftc1lem1  26010  ftc1a  26012  ftc1lem4  26014  ftc1lem5  26015  ftc1lem6  26016  ftc1  26017  ftc1cn  26018  ftc2  26019  ftc2ditglem  26020  ftc2ditg  26021  itgparts  26022  itgsubstlem  26023  itgpowd  26025  aalioulem3  26310  reeff1olem  26424  efcvx  26427  pilem3  26431  pige3ALT  26497  sinord  26511  recosf1o  26512  resinf1o  26513  efif1olem4  26522  asinrecl  26880  acosrecl  26881  emre  26984  pntlem3  27588  ttgcontlem1  28969  signsply0  34728  iblidicc  34769  ftc2re  34775  iccsconn  35461  iccllysconn  35463  cvmliftlem10  35507  ivthALT  36548  sin2h  37855  cos2h  37856  mblfinlem2  37903  ftc1cnnclem  37936  ftc1cnnc  37937  ftc1anclem7  37944  ftc1anc  37946  ftc2nc  37947  areacirclem2  37954  areacirclem3  37955  areacirclem4  37956  areacirc  37958  iccbnd  38085  icccmpALT  38086  arearect  43566  areaquad  43567  lhe4.4ex1a  44679  lefldiveq  45648  itgsin0pilem1  46302  ibliccsinexp  46303  iblioosinexp  46305  itgsinexplem1  46306  itgsinexp  46307  iblspltprt  46325  fourierdlem5  46464  fourierdlem9  46468  fourierdlem18  46477  fourierdlem24  46483  fourierdlem62  46520  fourierdlem66  46524  fourierdlem74  46532  fourierdlem75  46533  fourierdlem83  46541  fourierdlem87  46545  fourierdlem93  46551  fourierdlem95  46553  fourierdlem102  46560  fourierdlem103  46561  fourierdlem104  46562  fourierdlem112  46570  fourierdlem114  46572  sqwvfoura  46580  sqwvfourb  46581