Metamath Proof Explorer


Theorem atssbase

Description: The set of atoms is a subset of the base set. ( atssch analog.) (Contributed by NM, 21-Oct-2011)

Ref Expression
Hypotheses atombase.b
|- B = ( Base ` K )
atombase.a
|- A = ( Atoms ` K )
Assertion atssbase
|- A C_ B

Proof

Step Hyp Ref Expression
1 atombase.b
 |-  B = ( Base ` K )
2 atombase.a
 |-  A = ( Atoms ` K )
3 1 2 atbase
 |-  ( x e. A -> x e. B )
4 3 ssriv
 |-  A C_ B