Metamath Proof Explorer

Theorem sseq1i

Description: An equality inference for the subclass relationship. (Contributed by NM, 18-Aug-1993)

Ref Expression
Hypothesis sseq1i.1 
|- A = B
Assertion sseq1i 
|- ( A C_ C <-> B C_ C )

Proof

Step Hyp Ref Expression
1 sseq1i.1 
 |-  A = B
2 sseq1 
 |-  ( A = B -> ( A C_ C <-> B C_ C ) )
3 1 2 ax-mp 
 |-  ( A C_ C <-> B C_ C )