Theorem iccssre 13486

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 13468	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
2	1	biimp3a 1498	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))
3	2	simp1d 1160	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
4	3	3expia 1139	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ))
5	4	ssrdv 3940	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   ∈ wcel 2145   ⊆ wss 3902   class class class wbr 5107  (class class class)co 7417  ℝcr 11127   ≤ cle 11272  [,]cicc 13405

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-cnex 11184  ax-resscn 11185  ax-pre-lttri 11202  ax-pre-lttrn 11203

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7420  df-oprab 7421  df-mpo 7422  df-er 8700  df-en 8957  df-dom 8958  df-sdom 8959  df-pnf 11273  df-mnf 11274  df-xr 11275  df-ltxr 11276  df-le 11277  df-icc 13409

This theorem is used by:  iccssred  13491  iccsupr  13499  iccsplit  13542  iccshftri  13544  iccshftli  13546  iccdili  13548  icccntri  13550  unitssre  13556  supicc  13558  supiccub  13559  supicclub  13560  icccld  24998  iccntr  25054  icccmplem2  25056  icccmplem3  25057  icccmp  25058  retopconn  25062  iccconn  25063  cnmpopc  25162  iihalf1cn  25166  iihalf2cn  25168  icoopnst  25173  iocopnst  25174  icchmeo  25175  xrhmeo  25180  icccvx  25184  cnheiborlem  25188  htpycc  25214  pcocn  25251  pcohtpylem  25253  pcopt  25256  pcopt2  25257  pcoass  25258  pcorevlem  25260  ivthlem2  25686  ivthlem3  25687  ivthicc  25692  evthicc  25693  ovolficcss  25703  ovolicc1  25750  ovolicc2  25756  ovolicc  25757  iccmbl  25800  ovolioo  25802  dyadss  25828  volcn  25840  volivth  25841  vitalilem2  25843  vitalilem4  25845  mbfimaicc  25865  mbfi1fseqlem4  25952  itgioo  26050  rollelem  26223  rolle  26224  mvth  26226  dvlip  26227  c1liplem1  26230  c1lip1  26231  c1lip3  26233  dvgt0lem1  26236  dvgt0lem2  26237  dvgt0  26238  dvlt0  26239  dvge0  26240  dvle  26241  dvivthlem1  26242  dvivth  26244  dvne0  26245  lhop1lem  26247  dvcvx  26254  dvfsumge  26256  dvfsumabs  26257  ftc1lem1  26269  ftc1a  26271  ftc1lem4  26273  ftc1lem5  26274  ftc1lem6  26275  ftc1  26276  ftc1cn  26277  ftc2  26278  ftc2ditglem  26279  ftc2ditg  26280  itgparts  26281  itgsubstlem  26282  itgpowd  26284  aalioulem3  26577  reeff1olem  26689  efcvx  26692  pilem3  26696  pige3ALT  26765  sinord  26779  recosf1o  26780  resinf1o  26781  efif1olem4  26790  asinrecl  27147  acosrecl  27148  emre  27250  pntlem3  27853  ttgcontlem1  29349  signsply0  35067  iblidicc  35108  ftc2re  35114  iccsconn  35835  iccllysconn  35837  cvmliftlem10  35881  ivthALT  36962  sin2h  38372  cos2h  38373  mblfinlem2  38415  ftc1cnnclem  38448  ftc1cnnc  38449  ftc1anclem7  38456  ftc1anc  38458  ftc2nc  38459  areacirclem2  38466  areacirclem3  38467  areacirclem4  38468  areacirc  38470  iccbnd  38598  icccmpALT  38599  arearect  44064  areaquad  44065  lhe4.4ex1a  45161  lefldiveq  46133  itgsin0pilem1  46786  ibliccsinexp  46787  iblioosinexp  46789  itgsinexplem1  46790  itgsinexp  46791  iblspltprt  46809  fourierdlem5  46948  fourierdlem9  46952  fourierdlem18  46961  fourierdlem24  46967  fourierdlem62  47004  fourierdlem66  47008  fourierdlem74  47016  fourierdlem75  47017  fourierdlem83  47025  fourierdlem87  47029  fourierdlem93  47035  fourierdlem95  47037  fourierdlem102  47044  fourierdlem103  47045  fourierdlem104  47046  fourierdlem112  47054  fourierdlem114  47056  sqwvfoura  47064  sqwvfourb  47065