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 
|- ( A = B -> ( A C_ C <-> B C_ C ) )

Proof

Step Hyp Ref Expression
1 eqss 
 |-  ( A = B <-> ( A C_ B /\ B C_ A ) )
2 sstr2 
 |-  ( B C_ A -> ( A C_ C -> B C_ C ) )
3 sstr2 
 |-  ( A C_ B -> ( B C_ C -> A C_ C ) )
4 2 3 anbiim 
 |-  ( ( B C_ A /\ A C_ B ) -> ( A C_ C <-> B C_ C ) )
5 4 ancoms 
 |-  ( ( A C_ B /\ B C_ A ) -> ( A C_ C <-> B C_ C ) )
6 1 5 sylbi 
 |-  ( A = B -> ( A C_ C <-> B C_ C ) )