Colors of
variables: wff setvar class |
Syntax hints: wi 4 wb 176
wal 1540
wceq 1642
wcel 1710
cvv 2860
wss 3258
csn 3738 |
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-in 3214 df-ss 3260 df-sn 3742 |
This theorem is referenced by: snssg
3845 prss
3862 tpss
3872 sspwb
4119 elpw1
4145 nnsucelrlem3
4427 nnsucelr
4429 tfinnn
4535 vfinspeqtncv
4554 brssetsn
4760 fvimacnvi
5403 fvimacnv
5404 fnressn
5439 dfnnc3
5886 mapsn
6027 nc0le1
6217 frecxp
6315 |