![]() |
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 12527 | . . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) | |
2 | 1 | biimp3a 1599 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)) |
3 | 2 | simp1d 1178 | . . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ) |
4 | 3 | 3expia 1156 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ)) |
5 | 4 | ssrdv 3834 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1113 ∈ wcel 2166 ⊆ wss 3799 class class class wbr 4874 (class class class)co 6906 ℝcr 10252 ≤ cle 10393 [,]cicc 12467 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 ax-sep 5006 ax-nul 5014 ax-pow 5066 ax-pr 5128 ax-un 7210 ax-cnex 10309 ax-resscn 10310 ax-pre-lttri 10327 ax-pre-lttrn 10328 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3or 1114 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2606 df-eu 2641 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-ne 3001 df-nel 3104 df-ral 3123 df-rex 3124 df-rab 3127 df-v 3417 df-sbc 3664 df-csb 3759 df-dif 3802 df-un 3804 df-in 3806 df-ss 3813 df-nul 4146 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4660 df-br 4875 df-opab 4937 df-mpt 4954 df-id 5251 df-po 5264 df-so 5265 df-xp 5349 df-rel 5350 df-cnv 5351 df-co 5352 df-dm 5353 df-rn 5354 df-res 5355 df-ima 5356 df-iota 6087 df-fun 6126 df-fn 6127 df-f 6128 df-f1 6129 df-fo 6130 df-f1o 6131 df-fv 6132 df-ov 6909 df-oprab 6910 df-mpt2 6911 df-er 8010 df-en 8224 df-dom 8225 df-sdom 8226 df-pnf 10394 df-mnf 10395 df-xr 10396 df-ltxr 10397 df-le 10398 df-icc 12471 |
This theorem is referenced by: iccsupr 12556 iccsplit 12599 iccshftri 12601 iccshftli 12603 iccdili 12605 icccntri 12607 unitssre 12613 supicc 12614 supiccub 12615 supicclub 12616 icccld 22941 iccntr 22995 icccmplem2 22997 icccmplem3 22998 icccmp 22999 retopconn 23003 iccconn 23004 cnmpt2pc 23098 iihalf1cn 23102 iihalf2cn 23104 icoopnst 23109 iocopnst 23110 icchmeo 23111 xrhmeo 23116 icccvx 23120 cnheiborlem 23124 htpycc 23150 pcocn 23187 pcohtpylem 23189 pcopt 23192 pcopt2 23193 pcoass 23194 pcorevlem 23196 ivthlem2 23619 ivthlem3 23620 ivthicc 23625 evthicc 23626 ovolficcss 23636 ovolicc1 23683 ovolicc2 23689 ovolicc 23690 iccmbl 23733 ovolioo 23735 dyadss 23761 volcn 23773 volivth 23774 vitalilem2 23776 vitalilem4 23778 mbfimaicc 23798 mbfi1fseqlem4 23885 itgioo 23982 rollelem 24152 rolle 24153 cmvth 24154 mvth 24155 dvlip 24156 c1liplem1 24159 c1lip1 24160 c1lip3 24162 dvgt0lem1 24165 dvgt0lem2 24166 dvgt0 24167 dvlt0 24168 dvge0 24169 dvle 24170 dvivthlem1 24171 dvivth 24173 dvne0 24174 lhop1lem 24176 dvcvx 24183 dvfsumle 24184 dvfsumge 24185 dvfsumabs 24186 ftc1lem1 24198 ftc1a 24200 ftc1lem4 24202 ftc1lem5 24203 ftc1lem6 24204 ftc1 24205 ftc1cn 24206 ftc2 24207 ftc2ditglem 24208 ftc2ditg 24209 itgparts 24210 itgsubstlem 24211 aalioulem3 24489 reeff1olem 24600 efcvx 24603 pilem3 24607 pilem3OLD 24608 pige3 24670 sinord 24681 recosf1o 24682 resinf1o 24683 efif1olem4 24692 asinrecl 25043 acosrecl 25044 emre 25146 pntlem3 25712 ttgcontlem1 26185 signsply0 31176 iblidicc 31220 ftc2re 31226 iccsconn 31777 iccllysconn 31779 cvmliftlem10 31823 ivthALT 32869 sin2h 33943 cos2h 33944 mblfinlem2 33992 ftc1cnnclem 34027 ftc1cnnc 34028 ftc1anclem7 34035 ftc1anc 34037 ftc2nc 34038 areacirclem2 34045 areacirclem3 34046 areacirclem4 34047 areacirc 34049 iccbnd 34182 icccmpALT 34183 itgpowd 38643 arearect 38644 areaquad 38645 lhe4.4ex1a 39369 lefldiveq 40305 iccssred 40527 itgsin0pilem1 40961 ibliccsinexp 40962 iblioosinexp 40964 itgsinexplem1 40965 itgsinexp 40966 iblspltprt 40984 fourierdlem5 41124 fourierdlem9 41128 fourierdlem18 41137 fourierdlem24 41143 fourierdlem62 41180 fourierdlem66 41184 fourierdlem74 41192 fourierdlem75 41193 fourierdlem83 41201 fourierdlem87 41205 fourierdlem93 41211 fourierdlem95 41213 fourierdlem102 41220 fourierdlem103 41221 fourierdlem104 41222 fourierdlem112 41230 fourierdlem114 41232 sqwvfoura 41240 sqwvfourb 41241 |
Copyright terms: Public domain | W3C validator |