![]() |
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 13386 | . . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) | |
2 | 1 | biimp3a 1465 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)) |
3 | 2 | simp1d 1139 | . . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ) |
4 | 3 | 3expia 1118 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ)) |
5 | 4 | ssrdv 3980 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1084 ∈ wcel 2098 ⊆ wss 3940 class class class wbr 5138 (class class class)co 7401 ℝcr 11105 ≤ cle 11246 [,]cicc 13324 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-sep 5289 ax-nul 5296 ax-pow 5353 ax-pr 5417 ax-un 7718 ax-cnex 11162 ax-resscn 11163 ax-pre-lttri 11180 ax-pre-lttrn 11181 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-nel 3039 df-ral 3054 df-rex 3063 df-rab 3425 df-v 3468 df-sbc 3770 df-csb 3886 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-nul 4315 df-if 4521 df-pw 4596 df-sn 4621 df-pr 4623 df-op 4627 df-uni 4900 df-br 5139 df-opab 5201 df-mpt 5222 df-id 5564 df-po 5578 df-so 5579 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-ov 7404 df-oprab 7405 df-mpo 7406 df-er 8699 df-en 8936 df-dom 8937 df-sdom 8938 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-icc 13328 |
This theorem is referenced by: iccssred 13408 iccsupr 13416 iccsplit 13459 iccshftri 13461 iccshftli 13463 iccdili 13465 icccntri 13467 unitssre 13473 supicc 13475 supiccub 13476 supicclub 13477 icccld 24605 iccntr 24659 icccmplem2 24661 icccmplem3 24662 icccmp 24663 retopconn 24667 iccconn 24668 cnmpopc 24771 iihalf1cn 24775 iihalf1cnOLD 24776 iihalf2cn 24778 iihalf2cnOLD 24779 icoopnst 24785 iocopnst 24786 icchmeo 24787 icchmeoOLD 24788 xrhmeo 24793 icccvx 24797 cnheiborlem 24802 htpycc 24828 pcocn 24866 pcohtpylem 24868 pcopt 24871 pcopt2 24872 pcoass 24873 pcorevlem 24875 ivthlem2 25303 ivthlem3 25304 ivthicc 25309 evthicc 25310 ovolficcss 25320 ovolicc1 25367 ovolicc2 25373 ovolicc 25374 iccmbl 25417 ovolioo 25419 dyadss 25445 volcn 25457 volivth 25458 vitalilem2 25460 vitalilem4 25462 mbfimaicc 25482 mbfi1fseqlem4 25570 itgioo 25667 rollelem 25843 rolle 25844 cmvthOLD 25846 mvth 25847 dvlip 25848 c1liplem1 25851 c1lip1 25852 c1lip3 25854 dvgt0lem1 25857 dvgt0lem2 25858 dvgt0 25859 dvlt0 25860 dvge0 25861 dvle 25862 dvivthlem1 25863 dvivth 25865 dvne0 25866 lhop1lem 25868 dvcvx 25875 dvfsumleOLD 25877 dvfsumge 25878 dvfsumabs 25879 ftc1lem1 25892 ftc1a 25894 ftc1lem4 25896 ftc1lem5 25897 ftc1lem6 25898 ftc1 25899 ftc1cn 25900 ftc2 25901 ftc2ditglem 25902 ftc2ditg 25903 itgparts 25904 itgsubstlem 25905 itgpowd 25907 aalioulem3 26188 reeff1olem 26300 efcvx 26303 pilem3 26307 pige3ALT 26371 sinord 26385 recosf1o 26386 resinf1o 26387 efif1olem4 26396 asinrecl 26750 acosrecl 26751 emre 26854 pntlem3 27458 ttgcontlem1 28611 signsply0 34051 iblidicc 34093 ftc2re 34099 iccsconn 34728 iccllysconn 34730 cvmliftlem10 34774 ivthALT 35710 sin2h 36968 cos2h 36969 mblfinlem2 37016 ftc1cnnclem 37049 ftc1cnnc 37050 ftc1anclem7 37057 ftc1anc 37059 ftc2nc 37060 areacirclem2 37067 areacirclem3 37068 areacirclem4 37069 areacirc 37071 iccbnd 37198 icccmpALT 37199 arearect 42453 areaquad 42454 lhe4.4ex1a 43577 lefldiveq 44487 itgsin0pilem1 45151 ibliccsinexp 45152 iblioosinexp 45154 itgsinexplem1 45155 itgsinexp 45156 iblspltprt 45174 fourierdlem5 45313 fourierdlem9 45317 fourierdlem18 45326 fourierdlem24 45332 fourierdlem62 45369 fourierdlem66 45373 fourierdlem74 45381 fourierdlem75 45382 fourierdlem83 45390 fourierdlem87 45394 fourierdlem93 45400 fourierdlem95 45402 fourierdlem102 45409 fourierdlem103 45410 fourierdlem104 45411 fourierdlem112 45419 fourierdlem114 45421 sqwvfoura 45429 sqwvfourb 45430 |
Copyright terms: Public domain | W3C validator |