Theorem iccssre 13474

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   ∈ wcel 2146   ⊆ wss 3908   class class class wbr 5114  (class class class)co 7423  ℝcr 11117   ≤ cle 11262  [,]cicc 13393

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-cnex 11174  ax-resscn 11175  ax-pre-lttri 11192  ax-pre-lttrn 11193

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-po 5574  df-so 5575  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7426  df-oprab 7427  df-mpo 7428  df-er 8703  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11263  df-mnf 11264  df-xr 11265  df-ltxr 11266  df-le 11267  df-icc 13397

This theorem is used by:  iccssred  13479  iccsupr  13487  iccsplit  13530  iccshftri  13532  iccshftli  13534  iccdili  13536  icccntri  13538  unitssre  13544  supicc  13546  supiccub  13547  supicclub  13548  icccld  24960  iccntr  25016  icccmplem2  25018  icccmplem3  25019  icccmp  25020  retopconn  25024  iccconn  25025  cnmpopc  25124  iihalf1cn  25128  iihalf2cn  25130  icoopnst  25135  iocopnst  25136  icchmeo  25137  xrhmeo  25142  icccvx  25146  cnheiborlem  25150  htpycc  25176  pcocn  25213  pcohtpylem  25215  pcopt  25218  pcopt2  25219  pcoass  25220  pcorevlem  25222  ivthlem2  25648  ivthlem3  25649  ivthicc  25654  evthicc  25655  ovolficcss  25665  ovolicc1  25712  ovolicc2  25718  ovolicc  25719  iccmbl  25762  ovolioo  25764  dyadss  25790  volcn  25802  volivth  25803  vitalilem2  25805  vitalilem4  25807  mbfimaicc  25827  mbfi1fseqlem4  25914  itgioo  26012  rollelem  26185  rolle  26186  mvth  26188  dvlip  26189  c1liplem1  26192  c1lip1  26193  c1lip3  26195  dvgt0lem1  26198  dvgt0lem2  26199  dvgt0  26200  dvlt0  26201  dvge0  26202  dvle  26203  dvivthlem1  26204  dvivth  26206  dvne0  26207  lhop1lem  26209  dvcvx  26216  dvfsumge  26218  dvfsumabs  26219  ftc1lem1  26231  ftc1a  26233  ftc1lem4  26235  ftc1lem5  26236  ftc1lem6  26237  ftc1  26238  ftc1cn  26239  ftc2  26240  ftc2ditglem  26241  ftc2ditg  26242  itgparts  26243  itgsubstlem  26244  itgpowd  26246  aalioulem3  26534  reeff1olem  26646  efcvx  26649  pilem3  26653  pige3ALT  26722  sinord  26736  recosf1o  26737  resinf1o  26738  efif1olem4  26747  asinrecl  27104  acosrecl  27105  emre  27207  pntlem3  27810  ttgcontlem1  29271  signsply0  34969  iblidicc  35010  ftc2re  35016  iccsconn  35760  iccllysconn  35762  cvmliftlem10  35806  ivthALT  36886  sin2h  38301  cos2h  38302  mblfinlem2  38349  ftc1cnnclem  38382  ftc1cnnc  38383  ftc1anclem7  38390  ftc1anc  38392  ftc2nc  38393  areacirclem2  38400  areacirclem3  38401  areacirclem4  38402  areacirc  38404  iccbnd  38531  icccmpALT  38532  arearect  43982  areaquad  43983  lhe4.4ex1a  45079  lefldiveq  46051  itgsin0pilem1  46704  ibliccsinexp  46705  iblioosinexp  46707  itgsinexplem1  46708  itgsinexp  46709  iblspltprt  46727  fourierdlem5  46866  fourierdlem9  46870  fourierdlem18  46879  fourierdlem24  46885  fourierdlem62  46922  fourierdlem66  46926  fourierdlem74  46934  fourierdlem75  46935  fourierdlem83  46943  fourierdlem87  46947  fourierdlem93  46953  fourierdlem95  46955  fourierdlem102  46962  fourierdlem103  46963  fourierdlem104  46964  fourierdlem112  46972  fourierdlem114  46974  sqwvfoura  46982  sqwvfourb  46983