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 ⊆ B

Proof

Step Hyp Ref Expression
1 atombase.b ⊢ B = Base K
2 atombase.a ⊢ A = Atoms ⁡ K
3 1 2 atbase ⊢ x ∈ A → x ∈ B
4 3 ssriv ⊢ A ⊆ B