![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > restid | Structured version Visualization version Unicode version |
Description: The subspace topology of the base set is the original topology. (Contributed by Jeff Hankins, 9-Jul-2009.) (Revised by Mario Carneiro, 13-Aug-2015.) |
Ref | Expression |
---|---|
restid.1 |
![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
restid |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | restid.1 |
. . 3
![]() ![]() ![]() ![]() ![]() | |
2 | uniexg 6588 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl5eqel 2533 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1 | eqimss2i 3487 |
. . 3
![]() ![]() ![]() ![]() ![]() |
5 | sspwuni 4367 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 4, 5 | mpbir 213 |
. 2
![]() ![]() ![]() ![]() ![]() |
7 | restid2 15329 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 3, 6, 7 | sylancl 668 |
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 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-ral 2742 df-rex 2743 df-reu 2744 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-op 3975 df-uni 4199 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-id 4749 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-rest 15321 |
This theorem is referenced by: restin 20182 cnrmnrm 20377 cmpkgen 20566 xkopt 20670 xkoinjcn 20702 ussid 21275 tuslem 21282 cnperf 21838 retopcon 21847 cncfcn1 21942 cncfmpt2f 21946 cdivcncf 21949 abscncfALT 21952 cnmpt2pc 21956 cnrehmeo 21981 cnlimc 22843 recnperf 22860 dvidlem 22870 dvcnp2 22874 dvcn 22875 dvnres 22885 dvaddbr 22892 dvmulbr 22893 dvcobr 22900 dvcjbr 22903 dvrec 22909 dvexp3 22930 dveflem 22931 dvlipcn 22946 lhop1lem 22965 ftc1cn 22995 dvply1 23237 dvtaylp 23325 taylthlem2 23329 psercn 23381 pserdvlem2 23383 pserdv 23384 abelth 23396 logcn 23592 dvloglem 23593 dvlog 23596 dvlog2 23598 efopnlem2 23602 logtayl 23605 cxpcn 23685 cxpcn2 23686 cxpcn3 23688 resqrtcn 23689 sqrtcn 23690 dvatan 23861 ftalem3 23999 retopscon 29972 ivthALT 30991 dvtan 31992 ftc1cnnc 32016 dvasin 32028 dvacos 32029 binomcxplemdvbinom 36702 binomcxplemnotnn0 36705 fsumcncf 37755 ioccncflimc 37763 cncfuni 37764 icocncflimc 37767 cncfiooicclem1 37771 cxpcncf2 37778 itgsubsticclem 37852 dirkercncflem2 37966 dirkercncflem4 37968 fourierdlem32 38002 fourierdlem33 38003 fourierdlem62 38032 fourierdlem93 38063 fourierdlem101 38071 |
Copyright terms: Public domain | W3C validator |