Theorem sseq1i 3513

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 3510	. 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 184   = wceq 1383   C_ wss 3461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475

This theorem is referenced by:  eqsstri  3519  syl5eqss  3533  ssab  3555  rabss  3562  uniiunlem  3573  prss  4169  prssg  4170  sstp  4179  tpss  4180  iunss  4356  pwtr  4690  pwssun  4776  cores2  5510  dffun2  5588  sbcfg  5719  fnsuppresOLD  6116  idref  6138  ovmptss  6866  fnsuppres  6929  ordgt0ge1  7149  omopthlem1  7306  trcl  8162  rankbnd  8289  rankbnd2  8290  rankc1  8291  dfac12a  8531  fin23lem34  8729  axdc2lem  8831  alephval2  8950  indpi  9288  fsuppmapnn0fiublem  12078  0ram  14520  mreacs  15037  lsslinds  18844  2ndcctbss  19934  xkoinjcn  20166  restmetu  21068  xrlimcnp  23276  mptelee  24176  ausisusgra  24333  frgraunss  24973  n4cyclfrgra  24996  shlesb1i  26282  mdsldmd1i  27228  csmdsymi  27231  dfon2lem3  29193  dfon2lem7  29197  sspred  29228  trpredmintr  29290  filnetlem4  30175  cnvtrrel  37610  rp-imass  37617  dfhe3  37621