Theorem sseq1i 3488

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 3485	. 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 187   = wceq 1437   C_ wss 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450

This theorem is referenced by:  eqsstri  3494  syl5eqss  3508  ssab  3531  rabss  3538  uniiunlem  3549  prss  4154  prssg  4155  sstp  4164  tpss  4165  iunss  4340  pwtr  4674  pwssun  4759  cores2  5367  sspred  5407  dffun2  5611  sbcfg  5744  idref  6161  ovmptss  6888  fnsuppres  6953  ordgt0ge1  7210  omopthlem1  7367  trcl  8220  rankbnd  8347  rankbnd2  8348  rankc1  8349  dfac12a  8585  fin23lem34  8783  axdc2lem  8885  alephval2  9004  indpi  9339  fsuppmapnn0fiublem  12208  0ram  14977  mreacs  15563  lsslinds  19387  2ndcctbss  20468  xkoinjcn  20700  restmetu  21583  xrlimcnp  23892  mptelee  24923  ausisusgra  25080  frgraunss  25721  n4cyclfrgra  25744  shlesb1i  27037  mdsldmd1i  27982  csmdsymi  27985  dfon2lem3  30438  dfon2lem7  30442  trpredmintr  30479  filnetlem4  31042  ptrecube  31904  poimirlem30  31934  undmrnresiss  36180  clcnvlem  36200  ss2iundf  36221  cnvtrrel  36232  brtrclfv2  36289  rp-imass  36336  dfhe3  36340  dffrege76  36505  iunopeqop  38870  ausgrusgrb  39047  nbuhgr2vtx1edgblem  39184  nbgrsym  39202  isuvtxa  39226