Theorem iccssre 13489

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 13472	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
2	1	biimp3a 1469	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))
3	2	simp1d 1142	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
4	3	3expia 1121	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ))
5	4	ssrdv 4014	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   ∈ wcel 2108   ⊆ wss 3976   class class class wbr 5166  (class class class)co 7448  ℝcr 11183   ≤ cle 11325  [,]cicc 13410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-pre-lttri 11258  ax-pre-lttrn 11259

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-po 5607  df-so 5608  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-icc 13414

This theorem is referenced by:  iccssred  13494  iccsupr  13502  iccsplit  13545  iccshftri  13547  iccshftli  13549  iccdili  13551  icccntri  13553  unitssre  13559  supicc  13561  supiccub  13562  supicclub  13563  icccld  24808  iccntr  24862  icccmplem2  24864  icccmplem3  24865  icccmp  24866  retopconn  24870  iccconn  24871  cnmpopc  24974  iihalf1cn  24978  iihalf1cnOLD  24979  iihalf2cn  24981  iihalf2cnOLD  24982  icoopnst  24988  iocopnst  24989  icchmeo  24990  icchmeoOLD  24991  xrhmeo  24996  icccvx  25000  cnheiborlem  25005  htpycc  25031  pcocn  25069  pcohtpylem  25071  pcopt  25074  pcopt2  25075  pcoass  25076  pcorevlem  25078  ivthlem2  25506  ivthlem3  25507  ivthicc  25512  evthicc  25513  ovolficcss  25523  ovolicc1  25570  ovolicc2  25576  ovolicc  25577  iccmbl  25620  ovolioo  25622  dyadss  25648  volcn  25660  volivth  25661  vitalilem2  25663  vitalilem4  25665  mbfimaicc  25685  mbfi1fseqlem4  25773  itgioo  25871  rollelem  26047  rolle  26048  cmvthOLD  26050  mvth  26051  dvlip  26052  c1liplem1  26055  c1lip1  26056  c1lip3  26058  dvgt0lem1  26061  dvgt0lem2  26062  dvgt0  26063  dvlt0  26064  dvge0  26065  dvle  26066  dvivthlem1  26067  dvivth  26069  dvne0  26070  lhop1lem  26072  dvcvx  26079  dvfsumleOLD  26081  dvfsumge  26082  dvfsumabs  26083  ftc1lem1  26096  ftc1a  26098  ftc1lem4  26100  ftc1lem5  26101  ftc1lem6  26102  ftc1  26103  ftc1cn  26104  ftc2  26105  ftc2ditglem  26106  ftc2ditg  26107  itgparts  26108  itgsubstlem  26109  itgpowd  26111  aalioulem3  26394  reeff1olem  26508  efcvx  26511  pilem3  26515  pige3ALT  26580  sinord  26594  recosf1o  26595  resinf1o  26596  efif1olem4  26605  asinrecl  26963  acosrecl  26964  emre  27067  pntlem3  27671  ttgcontlem1  28917  signsply0  34528  iblidicc  34569  ftc2re  34575  iccsconn  35216  iccllysconn  35218  cvmliftlem10  35262  ivthALT  36301  sin2h  37570  cos2h  37571  mblfinlem2  37618  ftc1cnnclem  37651  ftc1cnnc  37652  ftc1anclem7  37659  ftc1anc  37661  ftc2nc  37662  areacirclem2  37669  areacirclem3  37670  areacirclem4  37671  areacirc  37673  iccbnd  37800  icccmpALT  37801  arearect  43176  areaquad  43177  lhe4.4ex1a  44298  lefldiveq  45207  itgsin0pilem1  45871  ibliccsinexp  45872  iblioosinexp  45874  itgsinexplem1  45875  itgsinexp  45876  iblspltprt  45894  fourierdlem5  46033  fourierdlem9  46037  fourierdlem18  46046  fourierdlem24  46052  fourierdlem62  46089  fourierdlem66  46093  fourierdlem74  46101  fourierdlem75  46102  fourierdlem83  46110  fourierdlem87  46114  fourierdlem93  46120  fourierdlem95  46122  fourierdlem102  46129  fourierdlem103  46130  fourierdlem104  46131  fourierdlem112  46139  fourierdlem114  46141  sqwvfoura  46149  sqwvfourb  46150