Definition df-ch0

Description: Define the zero for closed subspaces of Hilbert space. See h0elch for closure law. (Contributed by NM, 30-May-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	df-ch0	|- 0H = { 0h }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c0h	|- 0H
1		c0v	|- 0h
2	1	csn	|- { 0h }
3	0 2	wceq	|- 0H = { 0h }