Definition df-0p 21828

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 21827	. 2 class 0p
2		cc 9489	. . 3 class CC
3		cc0 9491	. . . 4 class 0
4	3	csn 4027	. . 3 class { 0 }
5	2, 4	cxp 4997	. 2 class ( CC X. { 0 } )
6	1, 5	wceq 1379	1 wff 0p = ( CC X. { 0 } )

This definition is referenced by:  0pval  21829  0plef  21830  0pledm  21831  itg1ge0  21844  mbfi1fseqlem5  21877  itg2addlem  21916  ply0  22356  coeeulem  22372  coe0  22403  dgr0  22409  dgreq0  22412  dgrmulc  22418  plymul0or  22427  plydiveu  22444  fta1lem  22453  fta1  22454  quotcan  22455  plyexmo  22459  elqaalem3  22467  aaliou2  22486  plymul02  28159  dgrnznn  30705  mpaaeu  30720