Theorem elicc2i 12110

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

Syntax hints:   ↔ wb 195   ∧ w3a 1031   ∈ wcel 1977   class class class wbr 4583  (class class class)co 6549  ℝcr 9814   ≤ cle 9954  [,]cicc 12049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-pre-lttri 9889  ax-pre-lttrn 9890

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-po 4959  df-so 4960  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-icc 12053

This theorem is referenced by:  0elunit  12161  1elunit  12162  divelunit  12185  lincmb01cmp  12186  iccf1o  12187  sinbnd2  14751  cosbnd2  14752  rpnnen2lem12  14793  blcvx  22409  iirev  22536  iihalf1  22538  iihalf2  22540  elii1  22542  elii2  22543  iimulcl  22544  iccpnfhmeo  22552  xrhmeo  22553  oprpiece1res2  22559  lebnumii  22573  htpycc  22587  pco0  22622  pcoval2  22624  pcocn  22625  pcohtpylem  22627  pcopt  22630  pcopt2  22631  pcoass  22632  pcorevlem  22634  vitalilem2  23184  vitali  23188  abelth2  24000  coseq00topi  24058  coseq0negpitopi  24059  sinq12ge0  24064  cosq14ge0  24067  cosordlem  24081  cosord  24082  cos11  24083  sinord  24084  recosf1o  24085  resinf1o  24086  efif1olem3  24094  argregt0  24160  argrege0  24161  argimgt0  24162  logimul  24164  cxpsqrtlem  24248  chordthmlem4  24362  acosbnd  24427  leibpi  24469  log2ub  24476  jensenlem2  24514  emcllem7  24528  emgt0  24533  harmonicbnd3  24534  harmoniclbnd  24535  harmonicubnd  24536  harmonicbnd4  24537  lgamgulmlem2  24556  logdivbnd  25045  pntpbnd2  25076  ttgcontlem1  25565  brbtwn2  25585  ax5seglem1  25608  ax5seglem2  25609  ax5seglem3  25611  ax5seglem5  25613  ax5seglem6  25614  ax5seglem9  25617  ax5seg  25618  axbtwnid  25619  axpaschlem  25620  axpasch  25621  axcontlem2  25645  axcontlem4  25647  axcontlem7  25650  stge0  28467  stle1  28468  strlem3a  28495  elunitrn  29271  elunitge0  29273  unitdivcld  29275  xrge0iifiso  29309  xrge0iifhom  29311  rescon  30482  snmlff  30565  sin2h  32569  cos2h  32570  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  lhe4.4ex1a  37550  fourierdlem40  39040  fourierdlem62  39061  fourierdlem78  39077  fourierdlem111  39110  sqwvfoura  39121  sqwvfourb  39122