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 2 adantl 
 |-  ( ( A C_ B /\ B C_ A ) -> ( A C_ C -> B C_ C ) )
4 sstr2 
 |-  ( A C_ B -> ( B C_ C -> A C_ C ) )
5 4 adantr 
 |-  ( ( A C_ B /\ B C_ A ) -> ( B C_ C -> A C_ C ) )
6 3 5 impbid 
 |-  ( ( A C_ B /\ B C_ A ) -> ( A C_ C <-> B C_ C ) )
7 1 6 sylbi 
 |-  ( A = B -> ( A C_ C <-> B C_ C ) )