Metamath Proof Explorer

Theorem sseq1

Description: Equality theorem for subclasses. (Contributed by NM, 24-Jun-1993) (Proof shortened by Andrew Salmon, 21-Jun-2011)

Ref Expression
Assertion sseq1 ( 𝐴 = 𝐵 → ( 𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 eqss ⊢ ( 𝐴 = 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) )
2 sstr2 ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶 ) )
3 sstr2 ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶 ) )
4 2 3 anbiim ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶 ) )
5 4 ancoms ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶 ) )
6 1 5 sylbi ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶 ) )