Theorem sseq1i 3073

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 3070	. 2 |- ( A = B -> ( A C_ C <-> B C_ C ) )
3	1, 2	ax-mp 7	1 |- ( A C_ C <-> B C_ C )

Syntax hints:   <-> wb 104   = wceq 1299   C_ wss 3021

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-11 1452  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-in 3027  df-ss 3034

This theorem is referenced by:  eqsstri  3079  syl5eqss  3093  ssab  3114  rabss  3121  uniiunlem  3132  prss  3623  prssg  3624  tpss  3632  iunss  3801  pwtr  4079  ordsucss  4358  elnn  4457  cores2  4987  dffun2  5069  funimaexglem  5142  idref  5590  ordgt0ge1  6262  prarloclemn  7208  bdeqsuc  12660  bj-omssind  12718