Theorem unitssre 13409

Description: (0[,]1) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.)

Assertion

Ref	Expression
unitssre	⊢ (0[,]1) ⊆ ℝ

Proof of Theorem unitssre

Step	Hyp	Ref	Expression
1		0re 11124	. 2 ⊢ 0 ∈ ℝ
2		1re 11122	. 2 ⊢ 1 ∈ ℝ
3		iccssre 13339	. 2 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ) → (0[,]1) ⊆ ℝ)
4	1, 2, 3	mp2an 692	1 ⊢ (0[,]1) ⊆ ℝ

Syntax hints:   ∈ wcel 2113   ⊆ wss 3899  (class class class)co 7355  ℝcr 11015  0cc0 11016  1c1 11017  [,]cicc 13258

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-cnex 11072  ax-resscn 11073  ax-1cn 11074  ax-icn 11075  ax-addcl 11076  ax-addrcl 11077  ax-mulcl 11078  ax-mulrcl 11079  ax-i2m1 11084  ax-1ne0 11085  ax-rnegex 11087  ax-rrecex 11088  ax-cnre 11089  ax-pre-lttri 11090  ax-pre-lttrn 11091

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7358  df-oprab 7359  df-mpo 7360  df-er 8631  df-en 8879  df-dom 8880  df-sdom 8881  df-pnf 11158  df-mnf 11159  df-xr 11160  df-ltxr 11161  df-le 11162  df-icc 13262

This theorem is referenced by:  unitsscn  13410  rpnnen  16146  iitopon  24809  dfii2  24812  dfii3  24813  dfii5  24815  iirevcn  24861  iihalf1cn  24863  iihalf1cnOLD  24864  iihalf2cn  24866  iihalf2cnOLD  24867  iimulcnOLD  24872  icchmeoOLD  24876  xrhmeo  24881  icccvx  24885  lebnumii  24902  reparphtiOLD  24934  pcoass  24961  pcorevlem  24963  pcorev2  24965  pi1xfrcnv  24994  vitalilem1  25546  vitalilem4  25549  vitalilem5  25550  vitali  25551  dvlipcn  25936  abelth2  26389  chordthmlem4  26782  chordthmlem5  26783  leibpi  26889  cvxcl  26932  scvxcvx  26933  lgamgulmlem2  26977  ttgcontlem1  28873  axeuclidlem  28951  stcl  32207  probun  34443  probvalrnd  34448  resconn  35301  cvmliftlem8  35347  poimirlem29  37699  poimirlem30  37700  poimirlem31  37701  poimir  37703  broucube  37704  k0004ss1  44258  k0004val0  44261  sqrlearg  45667  salgencntex  46455  eenglngeehlnmlem1  48852