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 13153 | . . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) | |
2 | 1 | biimp3a 1468 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)) |
3 | 2 | simp1d 1141 | . . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ) |
4 | 3 | 3expia 1120 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ)) |
5 | 4 | ssrdv 3928 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1086 ∈ wcel 2107 ⊆ wss 3888 class class class wbr 5075 (class class class)co 7284 ℝcr 10879 ≤ cle 11019 [,]cicc 13091 |
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 2710 ax-sep 5224 ax-nul 5231 ax-pow 5289 ax-pr 5353 ax-un 7597 ax-cnex 10936 ax-resscn 10937 ax-pre-lttri 10954 ax-pre-lttrn 10955 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-nel 3051 df-ral 3070 df-rex 3071 df-rab 3074 df-v 3435 df-sbc 3718 df-csb 3834 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-nul 4258 df-if 4461 df-pw 4536 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4841 df-br 5076 df-opab 5138 df-mpt 5159 df-id 5490 df-po 5504 df-so 5505 df-xp 5596 df-rel 5597 df-cnv 5598 df-co 5599 df-dm 5600 df-rn 5601 df-res 5602 df-ima 5603 df-iota 6395 df-fun 6439 df-fn 6440 df-f 6441 df-f1 6442 df-fo 6443 df-f1o 6444 df-fv 6445 df-ov 7287 df-oprab 7288 df-mpo 7289 df-er 8507 df-en 8743 df-dom 8744 df-sdom 8745 df-pnf 11020 df-mnf 11021 df-xr 11022 df-ltxr 11023 df-le 11024 df-icc 13095 |
This theorem is referenced by: iccssred 13175 iccsupr 13183 iccsplit 13226 iccshftri 13228 iccshftli 13230 iccdili 13232 icccntri 13234 unitssre 13240 supicc 13242 supiccub 13243 supicclub 13244 icccld 23939 iccntr 23993 icccmplem2 23995 icccmplem3 23996 icccmp 23997 retopconn 24001 iccconn 24002 cnmpopc 24100 iihalf1cn 24104 iihalf2cn 24106 icoopnst 24111 iocopnst 24112 icchmeo 24113 xrhmeo 24118 icccvx 24122 cnheiborlem 24126 htpycc 24152 pcocn 24189 pcohtpylem 24191 pcopt 24194 pcopt2 24195 pcoass 24196 pcorevlem 24198 ivthlem2 24625 ivthlem3 24626 ivthicc 24631 evthicc 24632 ovolficcss 24642 ovolicc1 24689 ovolicc2 24695 ovolicc 24696 iccmbl 24739 ovolioo 24741 dyadss 24767 volcn 24779 volivth 24780 vitalilem2 24782 vitalilem4 24784 mbfimaicc 24804 mbfi1fseqlem4 24892 itgioo 24989 rollelem 25162 rolle 25163 cmvth 25164 mvth 25165 dvlip 25166 c1liplem1 25169 c1lip1 25170 c1lip3 25172 dvgt0lem1 25175 dvgt0lem2 25176 dvgt0 25177 dvlt0 25178 dvge0 25179 dvle 25180 dvivthlem1 25181 dvivth 25183 dvne0 25184 lhop1lem 25186 dvcvx 25193 dvfsumle 25194 dvfsumge 25195 dvfsumabs 25196 ftc1lem1 25208 ftc1a 25210 ftc1lem4 25212 ftc1lem5 25213 ftc1lem6 25214 ftc1 25215 ftc1cn 25216 ftc2 25217 ftc2ditglem 25218 ftc2ditg 25219 itgparts 25220 itgsubstlem 25221 itgpowd 25223 aalioulem3 25503 reeff1olem 25614 efcvx 25617 pilem3 25621 pige3ALT 25685 sinord 25699 recosf1o 25700 resinf1o 25701 efif1olem4 25710 asinrecl 26061 acosrecl 26062 emre 26164 pntlem3 26766 ttgcontlem1 27261 signsply0 32539 iblidicc 32581 ftc2re 32587 iccsconn 33219 iccllysconn 33221 cvmliftlem10 33265 ivthALT 34533 sin2h 35776 cos2h 35777 mblfinlem2 35824 ftc1cnnclem 35857 ftc1cnnc 35858 ftc1anclem7 35865 ftc1anc 35867 ftc2nc 35868 areacirclem2 35875 areacirclem3 35876 areacirclem4 35877 areacirc 35879 iccbnd 36007 icccmpALT 36008 arearect 41053 areaquad 41054 lhe4.4ex1a 41954 lefldiveq 42838 itgsin0pilem1 43498 ibliccsinexp 43499 iblioosinexp 43501 itgsinexplem1 43502 itgsinexp 43503 iblspltprt 43521 fourierdlem5 43660 fourierdlem9 43664 fourierdlem18 43673 fourierdlem24 43679 fourierdlem62 43716 fourierdlem66 43720 fourierdlem74 43728 fourierdlem75 43729 fourierdlem83 43737 fourierdlem87 43741 fourierdlem93 43747 fourierdlem95 43749 fourierdlem102 43756 fourierdlem103 43757 fourierdlem104 43758 fourierdlem112 43766 fourierdlem114 43768 sqwvfoura 43776 sqwvfourb 43777 |
Copyright terms: Public domain | W3C validator |