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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
atombase.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion atssbase 𝐴 ⊆ 𝐵

Proof

Step Hyp Ref Expression
1 atombase.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 atombase.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 1 2 atbase ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 )
4 3 ssriv ⊢ 𝐴 ⊆ 𝐵