Metamath Proof Explorer

Theorem sseq2i

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

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

Proof

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