Colors of
variables: wff setvar class |
Syntax hints: wi 4 wb 176
wa 358
wceq 1642
wss 3258 |
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 |
This theorem is referenced by: sseq12
3295 sseq2i
3297 sseq2d
3300 syl5sseq
3320 nssne1
3328 psseq2
3358 sseq0
3583 un00
3587 disjpss
3602 pweq
3726 ssintab
3944 ssintub
3945 intmin
3947 p6eq
4239 opkelssetkg
4269 pw1equn
4332 pw1eqadj
4333 ssfin
4471 sfinltfin
4536 vfinspsslem1
4551 brssetg
4758 fununi
5161 funcnvuni
5162 feq3
5213 clos1induct
5881 frd
5923 nclec
6196 lecidg
6197 lecncvg
6200 ltcpw1pwg
6203 sbthlem2
6205 addlec
6209 nc0le1
6217 ce2le
6234 tlenc1c
6241 |