Colors of
variables: wff setvar class |
Syntax hints: wn 3
wb 176
wo 357
wa 358
wnan 1287
wcel 1710
cvv 2860
&ncap cnin 3205 ∼ ccompl 3206 cun 3208 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675
ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 |
This theorem depends on definitions:
df-bi 177 df-or 359
df-an 360 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2479 df-v 2862 df-nin 3212 df-compl 3213 df-un 3215 |
This theorem is referenced by: elsymdif
3224 uneqri
3407 uncom
3409 uneq1
3412 unass
3421 ssun1
3427 unss1
3433 ssequn1
3434 unss
3438 rexun
3444 ralunb
3445 indi
3502 undi
3503 unineq
3506 undif3
3516 symdif2
3521 rabun2
3535 reuun2
3539 undif4
3608 ssundif
3634 dfpr2
3750 eltpg
3770 pwpr
3884 pwtp
3885 unipr
3906 uniun
3911 intun
3959 iinun2
4033 iunun
4047 iunxun
4048 iinuni
4050 pwadjoin
4120 pw1un
4164 dfimak2
4299 dfaddc2
4382 nnsucelrlem1
4425 nnsucelrlem2
4426 nndisjeq
4430 ltfinex
4465 ltfintrilem1
4466 eqtfinrelk
4487 evenfinex
4504 oddfinex
4505 evenoddnnnul
4515 evenodddisjlem1
4516 nnadjoinlem1
4520 vfinspss
4552 vinf
4556 dfphi2
4570 dfop2lem1
4574 phi011lem1
4599 proj1op
4601 proj2op
4602 eqop
4612 brun
4693 setconslem2
4733 setconslem3
4734 setconslem7
4738 dfswap2
4742 xpundi
4833 xpundir
4834 dmun
4913 funun
5147 unpreima
5409 fvclss
5463 cupex
5817 clos1baseima
5884 connexex
5914 enadjlem1
6060 enadj
6061 enprmaplem4
6080 fce
6189 leconnnc
6219 nmembers1lem3
6271 nncdiv3lem2
6277 nchoicelem6
6295 nchoicelem18
6307 |