This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psseq2

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

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

Proof

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