Definition df-0p 22505

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 22504	. 2 class 0p
2		cc 9536	. . 3 class CC
3		cc0 9538	. . . 4 class 0
4	3	csn 4002	. . 3 class { 0 }
5	2, 4	cxp 4852	. 2 class ( CC X. { 0 } )
6	1, 5	wceq 1437	1 wff 0p = ( CC X. { 0 } )

This definition is referenced by:  0pval  22506  0plef  22507  0pledm  22508  itg1ge0  22521  mbfi1fseqlem5  22554  itg2addlem  22593  ply0  23030  coeeulem  23046  dgrnznn  23069  coe0  23078  dgr0  23084  dgreq0  23087  dgrmulc  23093  plymul0or  23102  plydiveu  23119  fta1lem  23128  fta1  23129  quotcan  23130  plyexmo  23134  elqaalem3  23142  aaliou2  23161  plymul02  29223  mpaaeu  35714