Definition df-0p 20989

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 20988	. 2 class 0p
2		cc 9267	. . 3 class CC
3		cc0 9269	. . . 4 class 0
4	3	csn 3865	. . 3 class { 0 }
5	2, 4	cxp 4825	. 2 class ( CC X. { 0 } )
6	1, 5	wceq 1362	1 wff 0p = ( CC X. { 0 } )

This definition is referenced by:  0pval  20990  0plef  20991  0pledm  20992  itg1ge0  21005  mbfi1fseqlem5  21038  itg2addlem  21077  ply0  21560  coeeulem  21576  coe0  21607  dgr0  21613  dgreq0  21616  dgrmulc  21622  plymul0or  21631  plydiveu  21648  fta1lem  21657  fta1  21658  quotcan  21659  plyexmo  21663  elqaalem3  21671  aaliou2  21690  plymul02  26794  dgrnznn  29334  mpaaeu  29349