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 2 adantl ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶 ) )
4 sstr2 ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶 ) )
5 4 adantr ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶 ) )
6 3 5 impbid ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶 ) )
7 1 6 sylbi ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶 ) )