Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > iccssre | Structured version Visualization version GIF version |
Description: A closed real interval is a set of reals. (Contributed by FL, 6-Jun-2007.) (Proof shortened by Paul Chapman, 21-Jan-2008.) |
Ref | Expression |
---|---|
iccssre | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elicc2 12109 | . . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) | |
2 | 1 | biimp3a 1424 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)) |
3 | 2 | simp1d 1066 | . . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ) |
4 | 3 | 3expia 1259 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ)) |
5 | 4 | ssrdv 3574 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 ∈ wcel 1977 ⊆ wss 3540 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: iccsupr 12137 iccsplit 12176 iccshftri 12178 iccshftli 12180 iccdili 12182 icccntri 12184 unitssre 12190 supicc 12191 supiccub 12192 supicclub 12193 icccld 22380 iccntr 22432 icccmplem2 22434 icccmplem3 22435 icccmp 22436 retopcon 22440 iccconn 22441 cnmpt2pc 22535 iihalf1cn 22539 iihalf2cn 22541 icoopnst 22546 iocopnst 22547 icchmeo 22548 xrhmeo 22553 icccvx 22557 cnheiborlem 22561 htpycc 22587 pcocn 22625 pcohtpylem 22627 pcopt 22630 pcopt2 22631 pcoass 22632 pcorevlem 22634 ivthlem2 23028 ivthlem3 23029 ivthicc 23034 evthicc 23035 ovolficcss 23045 ovolicc1 23091 ovolicc2 23097 ovolicc 23098 iccmbl 23141 ovolioo 23143 dyadss 23168 volcn 23180 volivth 23181 vitalilem2 23184 vitalilem4 23186 mbfimaicc 23206 mbfi1fseqlem4 23291 itgioo 23388 rollelem 23556 rolle 23557 cmvth 23558 mvth 23559 dvlip 23560 c1liplem1 23563 c1lip1 23564 c1lip3 23566 dvgt0lem1 23569 dvgt0lem2 23570 dvgt0 23571 dvlt0 23572 dvge0 23573 dvle 23574 dvivthlem1 23575 dvivth 23577 dvne0 23578 lhop1lem 23580 dvcvx 23587 dvfsumle 23588 dvfsumge 23589 dvfsumabs 23590 ftc1lem1 23602 ftc1a 23604 ftc1lem4 23606 ftc1lem5 23607 ftc1lem6 23608 ftc1 23609 ftc1cn 23610 ftc2 23611 ftc2ditglem 23612 ftc2ditg 23613 itgparts 23614 itgsubstlem 23615 aalioulem3 23893 reeff1olem 24004 efcvx 24007 pilem3 24011 pige3 24073 sinord 24084 recosf1o 24085 resinf1o 24086 efif1olem4 24095 asinrecl 24429 acosrecl 24430 emre 24532 pntlem3 25098 ttgcontlem1 25565 signsply0 29954 iccscon 30484 iccllyscon 30486 cvmliftlem10 30530 ivthALT 31500 sin2h 32569 cos2h 32570 mblfinlem2 32617 ftc1cnnclem 32653 ftc1cnnc 32654 ftc1anclem7 32661 ftc1anc 32663 ftc2nc 32664 areacirclem2 32671 areacirclem3 32672 areacirclem4 32673 areacirc 32675 iccbnd 32809 icccmpALT 32810 itgpowd 36819 arearect 36820 areaquad 36821 lhe4.4ex1a 37550 lefldiveq 38446 iccssred 38574 itgsin0pilem1 38841 ibliccsinexp 38842 iblioosinexp 38844 itgsinexplem1 38845 itgsinexp 38846 iblspltprt 38865 fourierdlem5 39005 fourierdlem9 39009 fourierdlem18 39018 fourierdlem24 39024 fourierdlem62 39061 fourierdlem66 39065 fourierdlem74 39073 fourierdlem75 39074 fourierdlem83 39082 fourierdlem87 39086 fourierdlem93 39092 fourierdlem95 39094 fourierdlem102 39101 fourierdlem103 39102 fourierdlem104 39103 fourierdlem112 39111 fourierdlem114 39113 sqwvfoura 39121 sqwvfourb 39122 |
Copyright terms: Public domain | W3C validator |