Theorem elicc2i 12432

Description: Inference for membership in a closed interval. (Contributed by Scott Fenton, 3-Jun-2013.)

Hypotheses

Ref	Expression
elicc2i.1	⊢ 𝐴 ∈ ℝ
elicc2i.2	⊢ 𝐵 ∈ ℝ

Assertion

Ref	Expression
elicc2i	⊢ (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))

Proof of Theorem elicc2i

Step	Hyp	Ref	Expression
1		elicc2i.1	. 2 ⊢ 𝐴 ∈ ℝ
2		elicc2i.2	. 2 ⊢ 𝐵 ∈ ℝ
3		elicc2 12431	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
4	1, 2, 3	mp2an 710	1 ⊢ (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))

Syntax hints:   ↔ wb 196   ∧ w3a 1072   ∈ wcel 2139   class class class wbr 4804  (class class class)co 6813  ℝcr 10127   ≤ cle 10267  [,]cicc 12371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185  ax-pre-lttri 10202  ax-pre-lttrn 10203

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-po 5187  df-so 5188  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-er 7911  df-en 8122  df-dom 8123  df-sdom 8124  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-icc 12375

This theorem is referenced by:  0elunit  12483  1elunit  12484  divelunit  12507  lincmb01cmp  12508  iccf1o  12509  sinbnd2  15111  cosbnd2  15112  rpnnen2lem12  15153  blcvx  22802  iirev  22929  iihalf1  22931  iihalf2  22933  elii1  22935  elii2  22936  iimulcl  22937  iccpnfhmeo  22945  xrhmeo  22946  oprpiece1res2  22952  lebnumii  22966  htpycc  22980  pco0  23014  pcoval2  23016  pcocn  23017  pcohtpylem  23019  pcopt  23022  pcopt2  23023  pcoass  23024  pcorevlem  23026  vitalilem2  23577  vitali  23581  abelth2  24395  coseq00topi  24453  coseq0negpitopi  24454  sinq12ge0  24459  cosq14ge0  24462  cosordlem  24476  cosord  24477  cos11  24478  sinord  24479  recosf1o  24480  resinf1o  24481  efif1olem3  24489  argregt0  24555  argrege0  24556  argimgt0  24557  logimul  24559  cxpsqrtlem  24647  chordthmlem4  24761  acosbnd  24826  leibpi  24868  log2ub  24875  jensenlem2  24913  emcllem7  24927  emgt0  24932  harmonicbnd3  24933  harmoniclbnd  24934  harmonicubnd  24935  harmonicbnd4  24936  lgamgulmlem2  24955  logdivbnd  25444  pntpbnd2  25475  ttgcontlem1  25964  brbtwn2  25984  ax5seglem1  26007  ax5seglem2  26008  ax5seglem3  26010  ax5seglem5  26012  ax5seglem6  26013  ax5seglem9  26016  ax5seg  26017  axbtwnid  26018  axpaschlem  26019  axpasch  26020  axcontlem2  26044  axcontlem4  26046  axcontlem7  26049  stge0  29392  stle1  29393  strlem3a  29420  elunitrn  30252  elunitge0  30254  unitdivcld  30256  xrge0iifiso  30290  xrge0iifhom  30292  resconn  31535  snmlff  31618  sin2h  33712  cos2h  33713  poimirlem29  33751  poimirlem30  33752  poimirlem31  33753  poimirlem32  33754  lhe4.4ex1a  39030  fourierdlem40  40867  fourierdlem62  40888  fourierdlem78  40904  fourierdlem111  40937  sqwvfoura  40948  sqwvfourb  40949