Theorem iccssre 13410

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 13393	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
2	1	biimp3a 1467	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))
3	2	simp1d 1140	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
4	3	3expia 1119	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ))
5	4	ssrdv 3987	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085   ∈ wcel 2104   ⊆ wss 3947   class class class wbr 5147  (class class class)co 7411  ℝcr 11111   ≤ cle 11253  [,]cicc 13331

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-pre-lttri 11186  ax-pre-lttrn 11187

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-icc 13335

This theorem is referenced by:  iccssred  13415  iccsupr  13423  iccsplit  13466  iccshftri  13468  iccshftli  13470  iccdili  13472  icccntri  13474  unitssre  13480  supicc  13482  supiccub  13483  supicclub  13484  icccld  24503  iccntr  24557  icccmplem2  24559  icccmplem3  24560  icccmp  24561  retopconn  24565  iccconn  24566  cnmpopc  24669  iihalf1cn  24673  iihalf1cnOLD  24674  iihalf2cn  24676  iihalf2cnOLD  24677  icoopnst  24683  iocopnst  24684  icchmeo  24685  icchmeoOLD  24686  xrhmeo  24691  icccvx  24695  cnheiborlem  24700  htpycc  24726  pcocn  24764  pcohtpylem  24766  pcopt  24769  pcopt2  24770  pcoass  24771  pcorevlem  24773  ivthlem2  25201  ivthlem3  25202  ivthicc  25207  evthicc  25208  ovolficcss  25218  ovolicc1  25265  ovolicc2  25271  ovolicc  25272  iccmbl  25315  ovolioo  25317  dyadss  25343  volcn  25355  volivth  25356  vitalilem2  25358  vitalilem4  25360  mbfimaicc  25380  mbfi1fseqlem4  25468  itgioo  25565  rollelem  25741  rolle  25742  cmvth  25743  mvth  25744  dvlip  25745  c1liplem1  25748  c1lip1  25749  c1lip3  25751  dvgt0lem1  25754  dvgt0lem2  25755  dvgt0  25756  dvlt0  25757  dvge0  25758  dvle  25759  dvivthlem1  25760  dvivth  25762  dvne0  25763  lhop1lem  25765  dvcvx  25772  dvfsumle  25773  dvfsumge  25774  dvfsumabs  25775  ftc1lem1  25787  ftc1a  25789  ftc1lem4  25791  ftc1lem5  25792  ftc1lem6  25793  ftc1  25794  ftc1cn  25795  ftc2  25796  ftc2ditglem  25797  ftc2ditg  25798  itgparts  25799  itgsubstlem  25800  itgpowd  25802  aalioulem3  26083  reeff1olem  26194  efcvx  26197  pilem3  26201  pige3ALT  26265  sinord  26279  recosf1o  26280  resinf1o  26281  efif1olem4  26290  asinrecl  26643  acosrecl  26644  emre  26746  pntlem3  27348  ttgcontlem1  28409  signsply0  33860  iblidicc  33902  ftc2re  33908  iccsconn  34537  iccllysconn  34539  cvmliftlem10  34583  ivthALT  35523  sin2h  36781  cos2h  36782  mblfinlem2  36829  ftc1cnnclem  36862  ftc1cnnc  36863  ftc1anclem7  36870  ftc1anc  36872  ftc2nc  36873  areacirclem2  36880  areacirclem3  36881  areacirclem4  36882  areacirc  36884  iccbnd  37011  icccmpALT  37012  arearect  42266  areaquad  42267  lhe4.4ex1a  43390  lefldiveq  44300  itgsin0pilem1  44964  ibliccsinexp  44965  iblioosinexp  44967  itgsinexplem1  44968  itgsinexp  44969  iblspltprt  44987  fourierdlem5  45126  fourierdlem9  45130  fourierdlem18  45139  fourierdlem24  45145  fourierdlem62  45182  fourierdlem66  45186  fourierdlem74  45194  fourierdlem75  45195  fourierdlem83  45203  fourierdlem87  45207  fourierdlem93  45213  fourierdlem95  45215  fourierdlem102  45222  fourierdlem103  45223  fourierdlem104  45224  fourierdlem112  45232  fourierdlem114  45234  sqwvfoura  45242  sqwvfourb  45243