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 12886 | . . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) | |
2 | 1 | biimp3a 1470 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)) |
3 | 2 | simp1d 1143 | . . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ) |
4 | 3 | 3expia 1122 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ)) |
5 | 4 | ssrdv 3883 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1088 ∈ wcel 2114 ⊆ wss 3843 class class class wbr 5030 (class class class)co 7170 ℝcr 10614 ≤ cle 10754 [,]cicc 12824 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2710 ax-sep 5167 ax-nul 5174 ax-pow 5232 ax-pr 5296 ax-un 7479 ax-cnex 10671 ax-resscn 10672 ax-pre-lttri 10689 ax-pre-lttrn 10690 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-nel 3039 df-ral 3058 df-rex 3059 df-rab 3062 df-v 3400 df-sbc 3681 df-csb 3791 df-dif 3846 df-un 3848 df-in 3850 df-ss 3860 df-nul 4212 df-if 4415 df-pw 4490 df-sn 4517 df-pr 4519 df-op 4523 df-uni 4797 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5429 df-po 5442 df-so 5443 df-xp 5531 df-rel 5532 df-cnv 5533 df-co 5534 df-dm 5535 df-rn 5536 df-res 5537 df-ima 5538 df-iota 6297 df-fun 6341 df-fn 6342 df-f 6343 df-f1 6344 df-fo 6345 df-f1o 6346 df-fv 6347 df-ov 7173 df-oprab 7174 df-mpo 7175 df-er 8320 df-en 8556 df-dom 8557 df-sdom 8558 df-pnf 10755 df-mnf 10756 df-xr 10757 df-ltxr 10758 df-le 10759 df-icc 12828 |
This theorem is referenced by: iccssred 12908 iccsupr 12916 iccsplit 12959 iccshftri 12961 iccshftli 12963 iccdili 12965 icccntri 12967 unitssre 12973 supicc 12975 supiccub 12976 supicclub 12977 icccld 23519 iccntr 23573 icccmplem2 23575 icccmplem3 23576 icccmp 23577 retopconn 23581 iccconn 23582 cnmpopc 23680 iihalf1cn 23684 iihalf2cn 23686 icoopnst 23691 iocopnst 23692 icchmeo 23693 xrhmeo 23698 icccvx 23702 cnheiborlem 23706 htpycc 23732 pcocn 23769 pcohtpylem 23771 pcopt 23774 pcopt2 23775 pcoass 23776 pcorevlem 23778 ivthlem2 24204 ivthlem3 24205 ivthicc 24210 evthicc 24211 ovolficcss 24221 ovolicc1 24268 ovolicc2 24274 ovolicc 24275 iccmbl 24318 ovolioo 24320 dyadss 24346 volcn 24358 volivth 24359 vitalilem2 24361 vitalilem4 24363 mbfimaicc 24383 mbfi1fseqlem4 24471 itgioo 24568 rollelem 24741 rolle 24742 cmvth 24743 mvth 24744 dvlip 24745 c1liplem1 24748 c1lip1 24749 c1lip3 24751 dvgt0lem1 24754 dvgt0lem2 24755 dvgt0 24756 dvlt0 24757 dvge0 24758 dvle 24759 dvivthlem1 24760 dvivth 24762 dvne0 24763 lhop1lem 24765 dvcvx 24772 dvfsumle 24773 dvfsumge 24774 dvfsumabs 24775 ftc1lem1 24787 ftc1a 24789 ftc1lem4 24791 ftc1lem5 24792 ftc1lem6 24793 ftc1 24794 ftc1cn 24795 ftc2 24796 ftc2ditglem 24797 ftc2ditg 24798 itgparts 24799 itgsubstlem 24800 itgpowd 24802 aalioulem3 25082 reeff1olem 25193 efcvx 25196 pilem3 25200 pige3ALT 25264 sinord 25278 recosf1o 25279 resinf1o 25280 efif1olem4 25289 asinrecl 25640 acosrecl 25641 emre 25743 pntlem3 26345 ttgcontlem1 26831 signsply0 32100 iblidicc 32142 ftc2re 32148 iccsconn 32781 iccllysconn 32783 cvmliftlem10 32827 ivthALT 34162 sin2h 35390 cos2h 35391 mblfinlem2 35438 ftc1cnnclem 35471 ftc1cnnc 35472 ftc1anclem7 35479 ftc1anc 35481 ftc2nc 35482 areacirclem2 35489 areacirclem3 35490 areacirclem4 35491 areacirc 35493 iccbnd 35621 icccmpALT 35622 arearect 40618 areaquad 40619 lhe4.4ex1a 41485 lefldiveq 42369 itgsin0pilem1 43033 ibliccsinexp 43034 iblioosinexp 43036 itgsinexplem1 43037 itgsinexp 43038 iblspltprt 43056 fourierdlem5 43195 fourierdlem9 43199 fourierdlem18 43208 fourierdlem24 43214 fourierdlem62 43251 fourierdlem66 43255 fourierdlem74 43263 fourierdlem75 43264 fourierdlem83 43272 fourierdlem87 43276 fourierdlem93 43282 fourierdlem95 43284 fourierdlem102 43291 fourierdlem103 43292 fourierdlem104 43293 fourierdlem112 43301 fourierdlem114 43303 sqwvfoura 43311 sqwvfourb 43312 |
Copyright terms: Public domain | W3C validator |