Metamath Proof Explorer

Theorem psseq1

Description: Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996)

Ref Expression
Assertion psseq1 ⊢ A = B → A ⊂ C ↔ B ⊂ C

Proof

Step Hyp Ref Expression
1 sseq1 ⊢ A = B → A ⊆ C ↔ B ⊆ C
2 neeq1 ⊢ A = B → A ≠ C ↔ B ≠ C
3 1 2 anbi12d ⊢ A = B → A ⊆ C ∧ A ≠ C ↔ B ⊆ C ∧ B ≠ C
4 df-pss ⊢ A ⊂ C ↔ A ⊆ C ∧ A ≠ C
5 df-pss ⊢ B ⊂ C ↔ B ⊆ C ∧ B ≠ C
6 3 4 5 3bitr4g ⊢ A = B → A ⊂ C ↔ B ⊂ C