![]() |
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 13389 | . . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) | |
2 | 1 | biimp3a 1470 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)) |
3 | 2 | simp1d 1143 | . . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ) |
4 | 3 | 3expia 1122 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ)) |
5 | 4 | ssrdv 3989 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1088 ∈ wcel 2107 ⊆ wss 3949 class class class wbr 5149 (class class class)co 7409 ℝcr 11109 ≤ cle 11249 [,]cicc 13327 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-cnex 11166 ax-resscn 11167 ax-pre-lttri 11184 ax-pre-lttrn 11185 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-po 5589 df-so 5590 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-ov 7412 df-oprab 7413 df-mpo 7414 df-er 8703 df-en 8940 df-dom 8941 df-sdom 8942 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 df-le 11254 df-icc 13331 |
This theorem is referenced by: iccssred 13411 iccsupr 13419 iccsplit 13462 iccshftri 13464 iccshftli 13466 iccdili 13468 icccntri 13470 unitssre 13476 supicc 13478 supiccub 13479 supicclub 13480 icccld 24283 iccntr 24337 icccmplem2 24339 icccmplem3 24340 icccmp 24341 retopconn 24345 iccconn 24346 cnmpopc 24444 iihalf1cn 24448 iihalf2cn 24450 icoopnst 24455 iocopnst 24456 icchmeo 24457 xrhmeo 24462 icccvx 24466 cnheiborlem 24470 htpycc 24496 pcocn 24533 pcohtpylem 24535 pcopt 24538 pcopt2 24539 pcoass 24540 pcorevlem 24542 ivthlem2 24969 ivthlem3 24970 ivthicc 24975 evthicc 24976 ovolficcss 24986 ovolicc1 25033 ovolicc2 25039 ovolicc 25040 iccmbl 25083 ovolioo 25085 dyadss 25111 volcn 25123 volivth 25124 vitalilem2 25126 vitalilem4 25128 mbfimaicc 25148 mbfi1fseqlem4 25236 itgioo 25333 rollelem 25506 rolle 25507 cmvth 25508 mvth 25509 dvlip 25510 c1liplem1 25513 c1lip1 25514 c1lip3 25516 dvgt0lem1 25519 dvgt0lem2 25520 dvgt0 25521 dvlt0 25522 dvge0 25523 dvle 25524 dvivthlem1 25525 dvivth 25527 dvne0 25528 lhop1lem 25530 dvcvx 25537 dvfsumle 25538 dvfsumge 25539 dvfsumabs 25540 ftc1lem1 25552 ftc1a 25554 ftc1lem4 25556 ftc1lem5 25557 ftc1lem6 25558 ftc1 25559 ftc1cn 25560 ftc2 25561 ftc2ditglem 25562 ftc2ditg 25563 itgparts 25564 itgsubstlem 25565 itgpowd 25567 aalioulem3 25847 reeff1olem 25958 efcvx 25961 pilem3 25965 pige3ALT 26029 sinord 26043 recosf1o 26044 resinf1o 26045 efif1olem4 26054 asinrecl 26407 acosrecl 26408 emre 26510 pntlem3 27112 ttgcontlem1 28142 signsply0 33562 iblidicc 33604 ftc2re 33610 iccsconn 34239 iccllysconn 34241 cvmliftlem10 34285 gg-iihalf1cn 35167 gg-iihalf2cn 35168 gg-icchmeo 35170 ivthALT 35220 sin2h 36478 cos2h 36479 mblfinlem2 36526 ftc1cnnclem 36559 ftc1cnnc 36560 ftc1anclem7 36567 ftc1anc 36569 ftc2nc 36570 areacirclem2 36577 areacirclem3 36578 areacirclem4 36579 areacirc 36581 iccbnd 36708 icccmpALT 36709 arearect 41964 areaquad 41965 lhe4.4ex1a 43088 lefldiveq 44002 itgsin0pilem1 44666 ibliccsinexp 44667 iblioosinexp 44669 itgsinexplem1 44670 itgsinexp 44671 iblspltprt 44689 fourierdlem5 44828 fourierdlem9 44832 fourierdlem18 44841 fourierdlem24 44847 fourierdlem62 44884 fourierdlem66 44888 fourierdlem74 44896 fourierdlem75 44897 fourierdlem83 44905 fourierdlem87 44909 fourierdlem93 44915 fourierdlem95 44917 fourierdlem102 44924 fourierdlem103 44925 fourierdlem104 44926 fourierdlem112 44934 fourierdlem114 44936 sqwvfoura 44944 sqwvfourb 44945 |
Copyright terms: Public domain | W3C validator |