Definition df-0p 22203

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 22202	. 2 class 0p
2		cc 9507	. . 3 class CC
3		cc0 9509	. . . 4 class 0
4	3	csn 4032	. . 3 class { 0 }
5	2, 4	cxp 5006	. 2 class ( CC X. { 0 } )
6	1, 5	wceq 1395	1 wff 0p = ( CC X. { 0 } )

This definition is referenced by:  0pval  22204  0plef  22205  0pledm  22206  itg1ge0  22219  mbfi1fseqlem5  22252  itg2addlem  22291  ply0  22731  coeeulem  22747  dgrnznn  22770  coe0  22779  dgr0  22785  dgreq0  22788  dgrmulc  22794  plymul0or  22803  plydiveu  22820  fta1lem  22829  fta1  22830  quotcan  22831  plyexmo  22835  elqaalem3  22843  aaliou2  22862  plymul02  28700  mpaaeu  31303