Theorem iccssre 13447

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 13429	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
2	1	biimp3a 1493	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))
3	2	simp1d 1158	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
4	3	3expia 1137	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ))
5	4	ssrdv 3945	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101   ∈ wcel 2145   ⊆ wss 3907   class class class wbr 5105  (class class class)co 7400  ℝcr 11087   ≤ cle 11232  [,]cicc 13366

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722  ax-cnex 11144  ax-resscn 11145  ax-pre-lttri 11162  ax-pre-lttrn 11163

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-po 5560  df-so 5561  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-ov 7403  df-oprab 7404  df-mpo 7405  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236  df-le 11237  df-icc 13370

This theorem is referenced by:  iccssred  13452  iccsupr  13460  iccsplit  13503  iccshftri  13505  iccshftli  13507  iccdili  13509  icccntri  13511  unitssre  13517  supicc  13519  supiccub  13520  supicclub  13521  icccld  24884  iccntr  24940  icccmplem2  24942  icccmplem3  24943  icccmp  24944  retopconn  24948  iccconn  24949  cnmpopc  25048  iihalf1cn  25052  iihalf2cn  25054  icoopnst  25059  iocopnst  25060  icchmeo  25061  xrhmeo  25066  icccvx  25070  cnheiborlem  25074  htpycc  25100  pcocn  25137  pcohtpylem  25139  pcopt  25142  pcopt2  25143  pcoass  25144  pcorevlem  25146  ivthlem2  25572  ivthlem3  25573  ivthicc  25578  evthicc  25579  ovolficcss  25589  ovolicc1  25636  ovolicc2  25642  ovolicc  25643  iccmbl  25686  ovolioo  25688  dyadss  25714  volcn  25726  volivth  25727  vitalilem2  25729  vitalilem4  25731  mbfimaicc  25751  mbfi1fseqlem4  25838  itgioo  25936  rollelem  26109  rolle  26110  mvth  26112  dvlip  26113  c1liplem1  26116  c1lip1  26117  c1lip3  26119  dvgt0lem1  26122  dvgt0lem2  26123  dvgt0  26124  dvlt0  26125  dvge0  26126  dvle  26127  dvivthlem1  26128  dvivth  26130  dvne0  26131  lhop1lem  26133  dvcvx  26140  dvfsumge  26142  dvfsumabs  26143  ftc1lem1  26155  ftc1a  26157  ftc1lem4  26159  ftc1lem5  26160  ftc1lem6  26161  ftc1  26162  ftc1cn  26163  ftc2  26164  ftc2ditglem  26165  ftc2ditg  26166  itgparts  26167  itgsubstlem  26168  itgpowd  26170  aalioulem3  26456  reeff1olem  26567  efcvx  26570  pilem3  26574  pige3ALT  26643  sinord  26657  recosf1o  26658  resinf1o  26659  efif1olem4  26668  asinrecl  27025  acosrecl  27026  emre  27128  pntlem3  27731  ttgcontlem1  29143  signsply0  34855  iblidicc  34896  ftc2re  34902  iccsconn  35611  iccllysconn  35613  cvmliftlem10  35657  ivthALT  36708  sin2h  38121  cos2h  38122  mblfinlem2  38169  ftc1cnnclem  38202  ftc1cnnc  38203  ftc1anclem7  38210  ftc1anc  38212  ftc2nc  38213  areacirclem2  38220  areacirclem3  38221  areacirclem4  38222  areacirc  38224  iccbnd  38351  icccmpALT  38352  arearect  43804  areaquad  43805  lhe4.4ex1a  44903  lefldiveq  45869  itgsin0pilem1  46522  ibliccsinexp  46523  iblioosinexp  46525  itgsinexplem1  46526  itgsinexp  46527  iblspltprt  46545  fourierdlem5  46684  fourierdlem9  46688  fourierdlem18  46697  fourierdlem24  46703  fourierdlem62  46740  fourierdlem66  46744  fourierdlem74  46752  fourierdlem75  46753  fourierdlem83  46761  fourierdlem87  46765  fourierdlem93  46771  fourierdlem95  46773  fourierdlem102  46780  fourierdlem103  46781  fourierdlem104  46782  fourierdlem112  46790  fourierdlem114  46792  sqwvfoura  46800  sqwvfourb  46801