![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iccss | Structured version Visualization version Unicode version |
Description: Condition for a closed interval to be a subset of another closed interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 20-Feb-2015.) |
Ref | Expression |
---|---|
iccss |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexr 9672 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | rexr 9672 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | anim12i 574 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | df-icc 11631 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | xrletr 11444 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | xrletr 11444 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 4, 4, 5, 6 | ixxss12 11644 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 3, 7 | sylan 478 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1672 ax-4 1685 ax-5 1761 ax-6 1808 ax-7 1854 ax-8 1892 ax-9 1899 ax-10 1918 ax-11 1923 ax-12 1936 ax-13 2091 ax-ext 2431 ax-sep 4496 ax-nul 4505 ax-pow 4553 ax-pr 4611 ax-un 6570 ax-cnex 9581 ax-resscn 9582 ax-pre-lttri 9599 ax-pre-lttrn 9600 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 987 df-3an 988 df-tru 1450 df-ex 1667 df-nf 1671 df-sb 1801 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-rab 2745 df-v 3014 df-sbc 3235 df-csb 3331 df-dif 3374 df-un 3376 df-in 3378 df-ss 3385 df-nul 3699 df-if 3849 df-pw 3920 df-sn 3936 df-pr 3938 df-op 3942 df-uni 4168 df-iun 4249 df-br 4374 df-opab 4433 df-mpt 4434 df-id 4726 df-po 4732 df-so 4733 df-xp 4817 df-rel 4818 df-cnv 4819 df-co 4820 df-dm 4821 df-rn 4822 df-res 4823 df-ima 4824 df-iota 5524 df-fun 5562 df-fn 5563 df-f 5564 df-f1 5565 df-fo 5566 df-f1o 5567 df-fv 5568 df-ov 6278 df-oprab 6279 df-mpt2 6280 df-1st 6780 df-2nd 6781 df-er 7349 df-en 7556 df-dom 7557 df-sdom 7558 df-pnf 9663 df-mnf 9664 df-xr 9665 df-ltxr 9666 df-le 9667 df-icc 11631 |
This theorem is referenced by: xrhmeo 21984 lebnumii 22007 pcoval1 22054 pcoval2 22057 ivthicc 22419 dyaddisjlem 22564 volsup2 22574 volcn 22575 mbfi1fseqlem5 22688 dvcvx 22983 dvfsumle 22984 dvfsumabs 22986 harmonicbnd3 23944 ppisval 24041 chtwordi 24094 ppiwordi 24100 chpub 24159 cvmliftlem2 30014 fourierdlem76 38102 fourierdlem103 38129 fourierdlem104 38130 fourierdlem107 38133 fourierdlem112 38138 salexct3 38257 salgensscntex 38259 |
Copyright terms: Public domain | W3C validator |