Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 = wceq 1542
∈ wcel 2107 ∖
cdif 3906 ⊆ wss 3909
∪ cuni 4864
‘cfv 6492 Topctop 22170
Clsdccld 22295 |
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 2709 ax-sep 5255 ax-nul 5262 ax-pow 5319 ax-pr 5383 ax-un 7663 |
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 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2888 df-ral 3064 df-rex 3073 df-rab 3407 df-v 3446 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-nul 4282 df-if 4486 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4865 df-br 5105 df-opab 5167 df-mpt 5188 df-id 5529 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-iota 6444 df-fun 6494 df-fn 6495 df-fv 6500 df-top 22171 df-cld 22298 |
This theorem is referenced by: cldss2
22309 iincld
22318 uncld
22320 cldcls
22321 iuncld
22324 clsval2
22329 clsss3
22338 clsss2
22351 opncldf1
22363 restcldr
22453 lmcld
22582 nrmsep2
22635 nrmsep
22636 isnrm2
22637 regsep2
22655 cmpcld
22681 dfconn2
22698 conncompclo
22714 cldllycmp
22774 txcld
22882 ptcld
22892 imasncld
22970 kqcldsat
23012 kqnrmlem1
23022 kqnrmlem2
23023 nrmhmph
23073 ufildr
23210 metnrmlem1a
24149 metnrmlem1
24150 metnrmlem2
24151 metnrmlem3
24152 cnheiborlem
24245 cmetss
24608 bcthlem5
24620 cldssbrsiga
32566 clsun
34731 cldregopn
34734 pibt2
35819 mblfinlem3
36048 mblfinlem4
36049 ismblfin
36050 cmpfiiin
40922 kelac1
41292 stoweidlem18
44050 stoweidlem57
44089 restcls2lem
46736 |