Colors of
variables: wff
setvar class |
Syntax hints:
↔ wb 205 = wceq 1542
⊆ wss 3949 ∅c0 4323 |
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 3477 df-dif 3952 df-in 3956 df-ss 3966 df-nul 4324 |
This theorem is referenced by: ss0
4399 un00
4443 pw0
4816 al0ssb
5309 fnsuppeq0
8177 cnfcom2lem
9696 card0
9953 kmlem5
10149 cf0
10246 fin1a2lem12
10406 mreexexlem3d
17590 efgval
19585 ppttop
22510 0nnei
22616 disjunsn
31825 isarchi
32328 filnetlem4
35266 bj-pw0ALT
35930 coss0
37349 pnonsingN
38804 osumcllem4N
38830 resnonrel
42343 ntrneicls11
42841 ntrneikb
42845 sprsymrelfvlem
46158 |