Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ wa 397
∈ wcel 2107 ≠
wne 2944 ∩ cin 3914
∅c0 4287 |
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 2708 |
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 2715 df-cleq 2729 df-clel 2815 df-ne 2945 df-v 3450 df-dif 3918 df-in 3922 df-nul 4288 |
This theorem is referenced by: minel
4430 disji
5093 disjiun
5097 onnseq
8295 uniinqs
8743 en3lplem1
9555 cplem1
9832 fpwwe2lem11
10584 limsupgre
15370 cat1lem
17989 lmcls
22669 conncn
22793 iunconnlem
22794 conncompclo
22802 2ndcsep
22826 lfinpfin
22891 locfincmp
22893 txcls
22971 pthaus
23005 qtopeu
23083 trfbas2
23210 filss
23220 zfbas
23263 fmfnfm
23325 tsmsfbas
23495 restmetu
23942 qdensere
24149 reperflem
24197 reconnlem1
24205 metds0
24229 metnrmlem1a
24237 minveclem3b
24808 ovolicc2lem5
24901 taylfval
25734 wlk1walk
28629 wwlksm1edg
28868 disjif
31538 disjif2
31541 subfacp1lem6
33819 erdszelem5
33829 pconnconn
33865 cvmseu
33910 neibastop2lem
34861 topdifinffinlem
35847 sstotbnd3
36264 brtrclfv2
42073 corcltrcl
42085 disjinfi
43486 |