Metamath Proof Explorer

Theorem sseq12i

Description: An equality inference for the subclass relationship. (Contributed by NM, 31-May-1999) (Proof shortened by Eric Schmidt, 26-Jan-2007)

Ref Expression
Hypotheses sseq1i.1 
|- A = B
sseq12i.2 
|- C = D
Assertion sseq12i 
|- ( A C_ C <-> B C_ D )

Proof

Step Hyp Ref Expression
1 sseq1i.1 
 |-  A = B
2 sseq12i.2 
 |-  C = D
3 sseq12 
 |-  ( ( A = B /\ C = D ) -> ( A C_ C <-> B C_ D ) )
4 1 2 3 mp2an 
 |-  ( A C_ C <-> B C_ D )