Metamath Proof Explorer

Theorem atcv0

Description: An atom covers the zero subspace. (Contributed by NM, 26-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion atcv0 
|- ( A e. HAtoms -> 0H

Proof

Step Hyp Ref Expression
1 ela 
 |-  ( A e. HAtoms <-> ( A e. CH /\ 0H
2 1 simprbi 
 |-  ( A e. HAtoms -> 0H