Colors of
variables: wff set class |
Syntax hints:
→ wi 4 ↔ wb 105
= wceq 1353 ⊆
wss 3129 |
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 3135 df-ss 3142 |
This theorem is referenced by: 3sstr3d
3199 3sstr4d
3200 ssdifeq0
3505 relcnvtr
5148 rdgisucinc
6385 oawordriexmid
6470 nnaword
6511 nnawordi
6515 sbthlem2
6956 isbth
6965 nninff
7120 infnninf
7121 infnninfOLD
7122 nnnninf
7123 nnnninfeq
7125 nnnninfeq2
7126 nninfwlpoimlemg
7172 ennnfonelemkh
12412 ennnfonelemrnh
12416 isstruct2im
12471 isstruct2r
12472 basis1
13517 baspartn
13520 eltg
13522 metss
13964 0nninf
14723 nnsf
14724 peano4nninf
14725 nninfalllem1
14727 nninfself
14732 |