Theorem sseq1i 3173

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

Hypothesis

Ref	Expression
sseq1i.1	|- A = B

Assertion

Ref	Expression
sseq1i	|- ( A C_ C <-> B C_ C )

Proof of Theorem sseq1i

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

Syntax hints:   <-> wb 104   = wceq 1348   C_ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  eqsstri  3179  eqsstrid  3193  ssab  3217  rabss  3224  uniiunlem  3236  prss  3734  prssg  3735  tpss  3743  iunss  3912  pwtr  4202  ordsucss  4486  elomssom  4587  cores2  5121  dffun2  5206  funimaexglem  5279  idref  5733  ordgt0ge1  6411  3nsssucpw1  7200  prarloclemn  7448  bdeqsuc  13876  bj-omssind  13930