Definition df-0p 21284

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 21283	. 2 class 0p
2		cc 9394	. . 3 class CC
3		cc0 9396	. . . 4 class 0
4	3	csn 3988	. . 3 class { 0 }
5	2, 4	cxp 4949	. 2 class ( CC X. { 0 } )
6	1, 5	wceq 1370	1 wff 0p = ( CC X. { 0 } )

This definition is referenced by:  0pval  21285  0plef  21286  0pledm  21287  itg1ge0  21300  mbfi1fseqlem5  21333  itg2addlem  21372  ply0  21812  coeeulem  21828  coe0  21859  dgr0  21865  dgreq0  21868  dgrmulc  21874  plymul0or  21883  plydiveu  21900  fta1lem  21909  fta1  21910  quotcan  21911  plyexmo  21915  elqaalem3  21923  aaliou2  21942  plymul02  27111  dgrnznn  29660  mpaaeu  29675