Theorem iccssre 13356

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087   ∈ wcel 2106   ⊆ wss 3913   class class class wbr 5110  (class class class)co 7362  ℝcr 11059   ≤ cle 11199  [,]cicc 13277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11116  ax-resscn 11117  ax-pre-lttri 11134  ax-pre-lttrn 11135

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-po 5550  df-so 5551  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-oprab 7366  df-mpo 7367  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11200  df-mnf 11201  df-xr 11202  df-ltxr 11203  df-le 11204  df-icc 13281

This theorem is referenced by:  iccssred  13361  iccsupr  13369  iccsplit  13412  iccshftri  13414  iccshftli  13416  iccdili  13418  icccntri  13420  unitssre  13426  supicc  13428  supiccub  13429  supicclub  13430  icccld  24167  iccntr  24221  icccmplem2  24223  icccmplem3  24224  icccmp  24225  retopconn  24229  iccconn  24230  cnmpopc  24328  iihalf1cn  24332  iihalf2cn  24334  icoopnst  24339  iocopnst  24340  icchmeo  24341  xrhmeo  24346  icccvx  24350  cnheiborlem  24354  htpycc  24380  pcocn  24417  pcohtpylem  24419  pcopt  24422  pcopt2  24423  pcoass  24424  pcorevlem  24426  ivthlem2  24853  ivthlem3  24854  ivthicc  24859  evthicc  24860  ovolficcss  24870  ovolicc1  24917  ovolicc2  24923  ovolicc  24924  iccmbl  24967  ovolioo  24969  dyadss  24995  volcn  25007  volivth  25008  vitalilem2  25010  vitalilem4  25012  mbfimaicc  25032  mbfi1fseqlem4  25120  itgioo  25217  rollelem  25390  rolle  25391  cmvth  25392  mvth  25393  dvlip  25394  c1liplem1  25397  c1lip1  25398  c1lip3  25400  dvgt0lem1  25403  dvgt0lem2  25404  dvgt0  25405  dvlt0  25406  dvge0  25407  dvle  25408  dvivthlem1  25409  dvivth  25411  dvne0  25412  lhop1lem  25414  dvcvx  25421  dvfsumle  25422  dvfsumge  25423  dvfsumabs  25424  ftc1lem1  25436  ftc1a  25438  ftc1lem4  25440  ftc1lem5  25441  ftc1lem6  25442  ftc1  25443  ftc1cn  25444  ftc2  25445  ftc2ditglem  25446  ftc2ditg  25447  itgparts  25448  itgsubstlem  25449  itgpowd  25451  aalioulem3  25731  reeff1olem  25842  efcvx  25845  pilem3  25849  pige3ALT  25913  sinord  25927  recosf1o  25928  resinf1o  25929  efif1olem4  25938  asinrecl  26289  acosrecl  26290  emre  26392  pntlem3  26994  ttgcontlem1  27896  signsply0  33252  iblidicc  33294  ftc2re  33300  iccsconn  33929  iccllysconn  33931  cvmliftlem10  33975  ivthALT  34883  sin2h  36141  cos2h  36142  mblfinlem2  36189  ftc1cnnclem  36222  ftc1cnnc  36223  ftc1anclem7  36230  ftc1anc  36232  ftc2nc  36233  areacirclem2  36240  areacirclem3  36241  areacirclem4  36242  areacirc  36244  iccbnd  36372  icccmpALT  36373  arearect  41607  areaquad  41608  lhe4.4ex1a  42731  lefldiveq  43647  itgsin0pilem1  44311  ibliccsinexp  44312  iblioosinexp  44314  itgsinexplem1  44315  itgsinexp  44316  iblspltprt  44334  fourierdlem5  44473  fourierdlem9  44477  fourierdlem18  44486  fourierdlem24  44492  fourierdlem62  44529  fourierdlem66  44533  fourierdlem74  44541  fourierdlem75  44542  fourierdlem83  44550  fourierdlem87  44554  fourierdlem93  44560  fourierdlem95  44562  fourierdlem102  44569  fourierdlem103  44570  fourierdlem104  44571  fourierdlem112  44579  fourierdlem114  44581  sqwvfoura  44589  sqwvfourb  44590