Theorem elicc2i 12430

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 12429	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
4	1, 2, 3	mp2an 710	1 ⊢ (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))

Syntax hints:   ↔ wb 196   ∧ w3a 1072   ∈ wcel 2137   class class class wbr 4802  (class class class)co 6811  ℝcr 10125   ≤ cle 10265  [,]cicc 12369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112  ax-cnex 10182  ax-resscn 10183  ax-pre-lttri 10200  ax-pre-lttrn 10201

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-nel 3034  df-ral 3053  df-rex 3054  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-op 4326  df-uni 4587  df-br 4803  df-opab 4863  df-mpt 4880  df-id 5172  df-po 5185  df-so 5186  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-iota 6010  df-fun 6049  df-fn 6050  df-f 6051  df-f1 6052  df-fo 6053  df-f1o 6054  df-fv 6055  df-ov 6814  df-oprab 6815  df-mpt2 6816  df-er 7909  df-en 8120  df-dom 8121  df-sdom 8122  df-pnf 10266  df-mnf 10267  df-xr 10268  df-ltxr 10269  df-le 10270  df-icc 12373

This theorem is referenced by:  0elunit  12481  1elunit  12482  divelunit  12505  lincmb01cmp  12506  iccf1o  12507  sinbnd2  15109  cosbnd2  15110  rpnnen2lem12  15151  blcvx  22800  iirev  22927  iihalf1  22929  iihalf2  22931  elii1  22933  elii2  22934  iimulcl  22935  iccpnfhmeo  22943  xrhmeo  22944  oprpiece1res2  22950  lebnumii  22964  htpycc  22978  pco0  23012  pcoval2  23014  pcocn  23015  pcohtpylem  23017  pcopt  23020  pcopt2  23021  pcoass  23022  pcorevlem  23024  vitalilem2  23575  vitali  23579  abelth2  24393  coseq00topi  24451  coseq0negpitopi  24452  sinq12ge0  24457  cosq14ge0  24460  cosordlem  24474  cosord  24475  cos11  24476  sinord  24477  recosf1o  24478  resinf1o  24479  efif1olem3  24487  argregt0  24553  argrege0  24554  argimgt0  24555  logimul  24557  cxpsqrtlem  24645  chordthmlem4  24759  acosbnd  24824  leibpi  24866  log2ub  24873  jensenlem2  24911  emcllem7  24925  emgt0  24930  harmonicbnd3  24931  harmoniclbnd  24932  harmonicubnd  24933  harmonicbnd4  24934  lgamgulmlem2  24953  logdivbnd  25442  pntpbnd2  25473  ttgcontlem1  25962  brbtwn2  25982  ax5seglem1  26005  ax5seglem2  26006  ax5seglem3  26008  ax5seglem5  26010  ax5seglem6  26011  ax5seglem9  26014  ax5seg  26015  axbtwnid  26016  axpaschlem  26017  axpasch  26018  axcontlem2  26042  axcontlem4  26044  axcontlem7  26047  stge0  29390  stle1  29391  strlem3a  29418  elunitrn  30250  elunitge0  30252  unitdivcld  30254  xrge0iifiso  30288  xrge0iifhom  30290  resconn  31533  snmlff  31616  sin2h  33710  cos2h  33711  poimirlem29  33749  poimirlem30  33750  poimirlem31  33751  poimirlem32  33752  lhe4.4ex1a  39028  fourierdlem40  40865  fourierdlem62  40886  fourierdlem78  40902  fourierdlem111  40935  sqwvfoura  40946  sqwvfourb  40947