Colors of
variables: wff setvar class |
Syntax hints: wn 3
wb 176
wcel 1710
cvv 2860
∼ ccompl 3206 |
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 |
This theorem is referenced by: dblcompl
3228 complab
3525 necompl
3545 sscon34
3662 disj5
3891 nincompl
4073 ssofss
4077 dfimak2
4299 dfint3
4319 dfpw2
4328 dfaddc2
4382 elsuc
4414 elsuci
4415 nnsucelrlem1
4425 nnsucelrlem3
4427 nnsucelr
4429 nndisjeq
4430 prepeano4
4452 preaddccan2lem1
4455 ltfinex
4465 ssfin
4471 eqpwrelk
4479 ncfinraiselem2
4481 ncfinraise
4482 ncfinlowerlem1
4483 ncfinlower
4484 eqtfinrelk
4487 tfinsuc
4499 evenfinex
4504 oddfinex
4505 evenodddisjlem1
4516 nnadjoinlem1
4520 nnadjoin
4521 nnpweqlem1
4523 srelk
4525 sfindbl
4531 sfintfinlem1
4532 tfinnnlem1
4534 tfinnn
4535 spfinex
4538 vfin1cltv
4548 nulnnn
4557 dfphi2
4570 dfop2lem1
4574 setconslem2
4733 setconslem3
4734 setconslem7
4738 dfswap2
4742 intirr
5030 brimage
5794 releqel
5808 disjex
5824 epprc
5828 funsex
5829 fnfullfunlem1
5857 fvfullfun
5865 transex
5911 refex
5912 antisymex
5913 connexex
5914 foundex
5915 extex
5916 symex
5917 qsexg
5983 enprmaplem4
6080 nenpw1pwlem1
6085 peano4nc
6151 ovcelem1
6172 ce0nn
6181 el2c
6192 tcfnex
6245 nclennlem1
6249 nnc3n3p1
6279 nchoicelem10
6299 nchoicelem11
6300 nchoicelem16
6305 nchoicelem18
6307 fnfreclem1
6318 |