Colors of
variables: wff
setvar class |
Syntax hints: {crab 3431 Vcvv 3472
⦋csb 3888
class class class wbr 5140 dom cdm 5668
Rel wrel 5673 ‘cfv 6531 (class class class)co 7392
finSupp cfsupp 9343 Basecbs 17125
↾s cress 17154 0gc0g 17366 mPwSer cmps 21385
mPoly cmpl 21387 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913
ax-6 1971 ax-7 2011 ax-8 2108
ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-sep 5291 ax-nul 5298 ax-pr 5419 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-rab 3432 df-v 3474 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-nul 4318 df-if 4522 df-sn 4622 df-pr 4624 df-op 4628 df-br 5141 df-opab 5203 df-xp 5674 df-rel 5675 df-dm 5678 df-oprab 7396 df-mpo 7397 df-mpl 21392 |
This theorem is referenced by: mplval
21476 mplrcl
21479 mplbaspropd
21687 ply1ascl
21708 mdegfval
25506 mdegcl
25513 |