Colors of
variables: wff set class |
Syntax hints: wcel 2158
(class class class)co 5888 cr 7824 c1 7826 caddc 7828 c4 8986 c5 8987 |
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 1457 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-4 1520 ax-17 1536 ax-ial 1544 ax-ext 2169 ax-1re 7919 ax-addrcl 7922 |
This theorem depends on definitions:
df-bi 117 df-cleq 2180 df-clel 2183 df-2 8992 df-3 8993
df-4 8994 df-5 8995 |
This theorem is referenced by: 5cn
9013 6re
9014 6pos
9034 3lt5
9109 2lt5
9110 1lt5
9111 5lt6
9112 4lt6
9113 5lt7
9118 4lt7
9119 5lt8
9125 4lt8
9126 5lt9
9133 4lt9
9134 5lt10
9532 4lt10
9533 5recm6rec
9541 ef01bndlem
11778 vscandxnscandx
12635 slotsdifipndx
12648 slotstnscsi
12668 plendxnscandx
12681 slotsdnscsi
12692 lgsdir2lem1
14725 |