Theorem iccssre 13380

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 13362	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
2	1	biimp3a 1477	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))
3	2	simp1d 1148	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
4	3	3expia 1127	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ))
5	4	ssrdv 3928	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092   ∈ wcel 2119   ⊆ wss 3890   class class class wbr 5079  (class class class)co 7363  ℝcr 11035   ≤ cle 11178  [,]cicc 13299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-cnex 11092  ax-resscn 11093  ax-pre-lttri 11110  ax-pre-lttrn 11111

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7366  df-oprab 7367  df-mpo 7368  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11179  df-mnf 11180  df-xr 11181  df-ltxr 11182  df-le 11183  df-icc 13303

This theorem is referenced by:  iccssred  13385  iccsupr  13393  iccsplit  13436  iccshftri  13438  iccshftli  13440  iccdili  13442  icccntri  13444  unitssre  13450  supicc  13452  supiccub  13453  supicclub  13454  icccld  24756  iccntr  24812  icccmplem2  24814  icccmplem3  24815  icccmp  24816  retopconn  24820  iccconn  24821  cnmpopc  24920  iihalf1cn  24924  iihalf2cn  24926  icoopnst  24931  iocopnst  24932  icchmeo  24933  xrhmeo  24938  icccvx  24942  cnheiborlem  24946  htpycc  24972  pcocn  25009  pcohtpylem  25011  pcopt  25014  pcopt2  25015  pcoass  25016  pcorevlem  25018  ivthlem2  25444  ivthlem3  25445  ivthicc  25450  evthicc  25451  ovolficcss  25461  ovolicc1  25508  ovolicc2  25514  ovolicc  25515  iccmbl  25558  ovolioo  25560  dyadss  25586  volcn  25598  volivth  25599  vitalilem2  25601  vitalilem4  25603  mbfimaicc  25623  mbfi1fseqlem4  25710  itgioo  25808  rollelem  25981  rolle  25982  mvth  25984  dvlip  25985  c1liplem1  25988  c1lip1  25989  c1lip3  25991  dvgt0lem1  25994  dvgt0lem2  25995  dvgt0  25996  dvlt0  25997  dvge0  25998  dvle  25999  dvivthlem1  26000  dvivth  26002  dvne0  26003  lhop1lem  26005  dvcvx  26012  dvfsumge  26014  dvfsumabs  26015  ftc1lem1  26027  ftc1a  26029  ftc1lem4  26031  ftc1lem5  26032  ftc1lem6  26033  ftc1  26034  ftc1cn  26035  ftc2  26036  ftc2ditglem  26037  ftc2ditg  26038  itgparts  26039  itgsubstlem  26040  itgpowd  26042  aalioulem3  26325  reeff1olem  26436  efcvx  26439  pilem3  26443  pige3ALT  26509  sinord  26523  recosf1o  26524  resinf1o  26525  efif1olem4  26534  asinrecl  26891  acosrecl  26892  emre  26994  pntlem3  27597  ttgcontlem1  28978  signsply0  34742  iblidicc  34783  ftc2re  34789  iccsconn  35483  iccllysconn  35485  cvmliftlem10  35529  ivthALT  36570  sin2h  37984  cos2h  37985  mblfinlem2  38032  ftc1cnnclem  38065  ftc1cnnc  38066  ftc1anclem7  38073  ftc1anc  38075  ftc2nc  38076  areacirclem2  38083  areacirclem3  38084  areacirclem4  38085  areacirc  38087  iccbnd  38214  icccmpALT  38215  arearect  43667  areaquad  43668  lhe4.4ex1a  44780  lefldiveq  45747  itgsin0pilem1  46400  ibliccsinexp  46401  iblioosinexp  46403  itgsinexplem1  46404  itgsinexp  46405  iblspltprt  46423  fourierdlem5  46562  fourierdlem9  46566  fourierdlem18  46575  fourierdlem24  46581  fourierdlem62  46618  fourierdlem66  46622  fourierdlem74  46630  fourierdlem75  46631  fourierdlem83  46639  fourierdlem87  46643  fourierdlem93  46649  fourierdlem95  46651  fourierdlem102  46658  fourierdlem103  46659  fourierdlem104  46660  fourierdlem112  46668  fourierdlem114  46670  sqwvfoura  46678  sqwvfourb  46679