Metamath Proof Explorer

Theorem elch0

Description: Membership in zero for closed subspaces of Hilbert space. (Contributed by NM, 6-Apr-2001) (New usage is discouraged.)

Ref Expression
Assertion elch0 
|- ( A e. 0H <-> A = 0h )

Proof

Step Hyp Ref Expression
1 df-ch0 
 |-  0H = { 0h }
2 1 eleq2i 
 |-  ( A e. 0H <-> A e. { 0h } )
3 ax-hv0cl 
 |-  0h e. ~H
4 3 elexi 
 |-  0h e. _V
5 4 elsn2 
 |-  ( A e. { 0h } <-> A = 0h )
6 2 5 bitri 
 |-  ( A e. 0H <-> A = 0h )