Colors of
variables: wff
setvar class |
Syntax hints:
∧ wa 397 = wceq 1542
∈ wcel 2107 ∩
cin 3948 ∅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-nul 4324 |
This theorem is referenced by: 0in
4394 csbin
4440 res0
5986 dfpo2
6296 predprc
6340 fresaun
6763 oev2
8523 dju0en
10170 ackbij1lem13
10227 ackbij1lem16
10230 incexclem
15782 bitsinv1
16383 bitsinvp1
16390 sadcadd
16399 sadadd2
16401 sadid1
16409 bitsres
16414 smumullem
16433 ressbas
17179 ressbasOLD
17180 sylow2a
19487 ablfac1eu
19943 indistopon
22504 fctop
22507 cctop
22509 rest0
22673 filconn
23387 volinun
25063 itg2cnlem2
25280 pthdlem2
29025 0pth
29378 1pthdlem2
29389 disjdifprg
31806 disjun0
31826 ofpreima2
31891 ldgenpisyslem1
33161 0elcarsg
33306 carsgclctunlem1
33316 carsgclctunlem3
33319 ballotlemfval0
33494 sate0
34406 elima4
34747 bj-rest10
35969 bj-rest0
35974 mblfinlem2
36526 conrel1d
42414 conrel2d
42415 ntrk0kbimka
42790 clsneibex
42853 neicvgbex
42863 qinioo
44248 nnfoctbdjlem
45171 caragen0
45222 |