Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ w3a 1088
= wceq 1542 ∈
wcel 2107 ≠ wne 2941
∀wral 3062 ∃wrex 3071 ∩ cin 3948
∅c0 4323 ∪ cuni 4909 Topctop 22395
Hauscha 22812 |
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 3063 df-rex 3072 df-rab 3434 df-v 3477 df-in 3956 df-ss 3966 df-uni 4910 df-haus 22819 |
This theorem is referenced by: haust1
22856 resthaus
22872 sshaus
22879 lmmo
22884 hauscmplem
22910 hauscmp
22911 hauslly
22996 hausllycmp
22998 kgenhaus
23048 pthaus
23142 txhaus
23151 xkohaus
23157 haushmph
23296 cmphaushmeo
23304 hausflim
23485 hauspwpwf1
23491 hauspwpwdom
23492 hausflf
23501 cnextfun
23568 cnextfvval
23569 cnextf
23570 cnextcn
23571 cnextfres1
23572 cnextfres
23573 qtophaus
32816 ismntop
33006 poimirlem30
36518 hausgraph
41954 |