Theorem sseq1i 3468

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 3465	. 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 189   = wceq 1455   C_ wss 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-in 3423  df-ss 3430

This theorem is referenced by:  eqsstri  3474  syl5eqss  3488  ssab  3511  rabss  3518  uniiunlem  3529  prss  4139  prssg  4140  sstp  4149  tpss  4150  iunss  4333  pwtr  4670  pwssun  4762  cores2  5371  sspred  5411  dffun2  5615  sbcfg  5753  idref  6176  ovmptss  6909  fnsuppres  6974  ordgt0ge1  7230  omopthlem1  7387  trcl  8243  rankbnd  8370  rankbnd2  8371  rankc1  8372  dfac12a  8609  fin23lem34  8807  axdc2lem  8909  alephval2  9028  indpi  9363  fsuppmapnn0fiublem  12240  0ram  15033  mreacs  15619  lsslinds  19444  2ndcctbss  20525  xkoinjcn  20757  restmetu  21640  xrlimcnp  23950  mptelee  24981  ausisusgra  25138  frgraunss  25779  n4cyclfrgra  25802  shlesb1i  27095  mdsldmd1i  28040  csmdsymi  28043  dfon2lem3  30481  dfon2lem7  30485  trpredmintr  30522  filnetlem4  31087  ptrecube  31986  poimirlem30  32016  undmrnresiss  36256  clcnvlem  36276  ss2iundf  36297  cnvtrrel  36308  brtrclfv2  36365  rp-imass  36412  dfhe3  36416  dffrege76  36581  iunssf  37481  iunopeqop  39141  ausgrusgrb  39396  nbuhgr2vtx1edgblem  39565  nbgrsym  39583  isuvtxa  39613  21wlkdlem6  39976