Colors of
variables: wff
setvar class |
Syntax hints:
= wceq 1542 ∩ cin 3910
∅c0 4283 |
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-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3407 df-v 3446 df-dif 3914 df-in 3918 df-nul 4284 |
This theorem is referenced by: pred0
6290 fresaunres2
6715 fnsuppeq0
8124 setsfun
17048 setsfun0
17049 indistopon
22367 fctop
22370 cctop
22372 restsn
22537 filconn
23250 chtdif
26523 ppidif
26528 ppi1
26529 cht1
26530 0res
31568 ofpreima2
31628 ordtconnlem1
32562 measvuni
32870 measinb
32877 cndprobnul
33094 ballotlemfp1
33148 ballotlemgun
33181 chtvalz
33299 mrsubvrs
34173 mblfinlem2
36162 ntrkbimka
42398 neicvgbex
42472 limsup0
44021 subsalsal
44686 nnfoctbdjlem
44782 |