This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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