Colors of
variables: wff
setvar class |
Syntax hints:
↔ wb 205 = wceq 1542
⊆ wss 3911 ∅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-v 3446 df-dif 3914 df-in 3918 df-ss 3928 df-nul 4284 |
This theorem is referenced by: ss0
4359 un00
4403 pw0
4773 al0ssb
5266 fnsuppeq0
8124 cnfcom2lem
9642 card0
9899 kmlem5
10095 cf0
10192 fin1a2lem12
10352 mreexexlem3d
17531 efgval
19504 ppttop
22373 0nnei
22479 disjunsn
31558 isarchi
32067 filnetlem4
34899 bj-pw0ALT
35566 coss0
36987 pnonsingN
38442 osumcllem4N
38468 resnonrel
41952 ntrneicls11
42450 ntrneikb
42454 sprsymrelfvlem
45768 |