Metamath Proof Explorer

Theorem eqimss

Description: Equality implies inclusion. (Contributed by NM, 21-Jun-1993) (Proof shortened by Andrew Salmon, 21-Jun-2011)

Ref Expression
Assertion eqimss ( 𝐴 = 𝐵 → 𝐴 ⊆ 𝐵 )

Proof

Step Hyp Ref Expression
1 eqss ⊢ ( 𝐴 = 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) )
2 1 simplbi ⊢ ( 𝐴 = 𝐵 → 𝐴 ⊆ 𝐵 )