Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ w3a 1088
= wceq 1542 ∈
wcel 2107 ≠ wne 2940
∀wral 3061 ∃wrex 3070 ∩ cin 3913
∅c0 4286 ∪ cuni 4869 Topctop 22265
Hauscha 22682 |
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-ext 2704 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3062 df-rex 3071 df-rab 3407 df-v 3449 df-in 3921 df-ss 3931 df-uni 4870 df-haus 22689 |
This theorem is referenced by: haust1
22726 resthaus
22742 sshaus
22749 lmmo
22754 hauscmplem
22780 hauscmp
22781 hauslly
22866 hausllycmp
22868 kgenhaus
22918 pthaus
23012 txhaus
23021 xkohaus
23027 haushmph
23166 cmphaushmeo
23174 hausflim
23355 hauspwpwf1
23361 hauspwpwdom
23362 hausflf
23371 cnextfun
23438 cnextfvval
23439 cnextf
23440 cnextcn
23441 cnextfres1
23442 cnextfres
23443 qtophaus
32481 ismntop
32671 poimirlem30
36158 hausgraph
41586 |