Colors of
variables: wff set class |
Syntax hints: wi 4
wal 1351
wcel 2148
wss 3131 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-7 1448
ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-11 1506 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions:
df-bi 117 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-in 3137 df-ss 3144 |
This theorem is referenced by: sstr
3165 sstri
3166 sseq1
3180 sseq2
3181 ssun3
3302 ssun4
3303 ssinss1
3366 ssdisj
3481 triun
4116 trintssm
4119 sspwb
4218 exss
4229 relss
4715 funss
5237 funimass2
5296 fss
5379 fiintim
6930 sbthlem2
6959 sbthlemi3
6960 sbthlemi6
6963 lsslss
13473 tgss
13602 tgcl
13603 tgss3
13617 clsss
13657 neiss
13689 ssnei2
13696 cnpnei
13758 cnptopco
13761 cnptoprest
13778 txcnp
13810 neibl
14030 metcnp3
14050 bj-nntrans
14742 |