Definition df-0p 22677

Description: Define the zero polynomial. (Contributed by Mario Carneiro, 19-Jun-2014.)

Assertion

Ref	Expression
df-0p	|- 0p = ( CC X. { 0 } )

Detailed syntax breakdown of Definition df-0p

Step	Hyp	Ref	Expression
1		c0p 22676	. 2 class 0p
2		cc 9563	. . 3 class CC
3		cc0 9565	. . . 4 class 0
4	3	csn 3980	. . 3 class { 0 }
5	2, 4	cxp 4851	. 2 class ( CC X. { 0 } )
6	1, 5	wceq 1455	1 wff 0p = ( CC X. { 0 } )

This definition is referenced by:  0pval  22678  0plef  22679  0pledm  22680  itg1ge0  22693  mbfi1fseqlem5  22726  itg2addlem  22765  ply0  23211  coeeulem  23227  dgrnznn  23250  coe0  23259  dgr0  23265  dgreq0  23268  dgrmulc  23274  plymul0or  23283  plydiveu  23300  fta1lem  23309  fta1  23310  quotcan  23311  plyexmo  23315  elqaalem3  23323  elqaalem3OLD  23326  aaliou2  23345  plymul02  29484  mpaaeu  36061