Definition df-0p 21123

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 21122	. 2 class 0p
2		cc 9272	. . 3 class CC
3		cc0 9274	. . . 4 class 0
4	3	csn 3872	. . 3 class { 0 }
5	2, 4	cxp 4833	. 2 class ( CC X. { 0 } )
6	1, 5	wceq 1369	1 wff 0p = ( CC X. { 0 } )

This definition is referenced by:  0pval  21124  0plef  21125  0pledm  21126  itg1ge0  21139  mbfi1fseqlem5  21172  itg2addlem  21211  ply0  21651  coeeulem  21667  coe0  21698  dgr0  21704  dgreq0  21707  dgrmulc  21713  plymul0or  21722  plydiveu  21739  fta1lem  21748  fta1  21749  quotcan  21750  plyexmo  21754  elqaalem3  21762  aaliou2  21781  plymul02  26899  dgrnznn  29445  mpaaeu  29460