Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ wa 397
= wceq 1542 ∈
wcel 2107 {crab 3406
⊆ wss 3914 ∪ cuni 4869 ∩ cint 4911 ‘cfv 6500
Topctop 22265 Clsdccld 22390
clsccl 22392 |
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-rep 5246 ax-sep 5260 ax-nul 5267 ax-pow 5324 ax-pr 5388 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 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 2941 df-ral 3062 df-rex 3071 df-reu 3353 df-rab 3407 df-v 3449 df-sbc 3744 df-csb 3860 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4287 df-if 4491 df-pw 4566 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4870 df-int 4912 df-iun 4960 df-br 5110 df-opab 5172 df-mpt 5193 df-id 5535 df-xp 5643 df-rel 5644 df-cnv 5645 df-co 5646 df-dm 5647 df-rn 5648 df-res 5649 df-ima 5650 df-iota 6452 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-top 22266 df-cld 22393 df-cls 22395 |
This theorem is referenced by: iscld4
22439 elcls
22447 ntrcls0
22450 clslp
22522 restcls
22555 cncls2i
22644 nrmsep
22731 lpcls
22738 regsep2
22750 hauscmplem
22780 hauscmp
22781 clsconn
22804 conncompcld
22808 hausllycmp
22868 txcls
22978 ptclsg
22989 regr1lem
23113 kqreglem1
23115 kqreglem2
23116 kqnrmlem1
23117 kqnrmlem2
23118 fclscmpi
23403 flfcntr
23417 cnextfres
23443 clssubg
23483 tsmsid
23514 cnllycmp
24342 clsocv
24637 relcmpcmet
24705 bcthlem2
24712 bcthlem4
24714 limcnlp
25265 opnbnd
34850 opnregcld
34855 cldregopn
34856 heibor1lem
36318 heiborlem8
36327 sepdisj
47047 iscnrm3rlem4
47066 |