Theorem sseq1i 3332

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

Syntax hints:   <-> wb 177   = wceq 1649   C_ wss 3280

This theorem is referenced by:  eqsstri  3338  syl5eqss  3352  ssab  3373  rabss  3380  uniiunlem  3391  prss  3912  prssg  3913  sstp  3923  tpss  3924  iunss  4092  pwtr  4376  pwssun  4449  cores2  5341  dffun2  5423  fnsuppres  5911  idref  5938  ovmptss  6387  ordgt0ge1  6700  omopthlem1  6857  trcl  7620  rankbnd  7750  rankbnd2  7751  rankc1  7752  dfac12a  7984  fin23lem34  8182  axdc2lem  8284  alephval2  8403  indpi  8740  0ram  13343  mreacs  13838  2ndcctbss  17471  xkoinjcn  17672  restmetu  18570  xrlimcnp  20760  ausisusgra  21333  shlesb1i  22841  mdsldmd1i  23787  csmdsymi  23790  dfon2lem3  25355  dfon2lem7  25359  sspred  25388  trpredmintr  25448  mptelee  25738  filnetlem4  26300  lsslinds  27169  frgraunss  28099  n4cyclfrgra  28122

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294