Theorem sseq1i 3375

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 3372	. 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 1369   C_ wss 3323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337

This theorem is referenced by:  eqsstri  3381  syl5eqss  3395  ssab  3417  rabss  3424  uniiunlem  3435  prss  4022  prssg  4023  sstp  4032  tpss  4033  iunss  4206  pwtr  4540  pwssun  4622  cores2  5345  dffun2  5423  sbcfg  5552  fnsuppresOLD  5933  idref  5953  ovmptss  6649  fnsuppres  6711  ordgt0ge1  6929  omopthlem1  7086  trcl  7940  rankbnd  8067  rankbnd2  8068  rankc1  8069  dfac12a  8309  fin23lem34  8507  axdc2lem  8609  alephval2  8728  indpi  9068  0ram  14073  mreacs  14588  lsslinds  18240  2ndcctbss  19039  xkoinjcn  19240  restmetu  20142  xrlimcnp  22342  mptelee  23109  ausisusgra  23247  shlesb1i  24757  mdsldmd1i  25703  csmdsymi  25706  dfon2lem3  27567  dfon2lem7  27571  sspred  27602  trpredmintr  27664  filnetlem4  28573  frgraunss  30558  n4cyclfrgra  30581  fsuppmapnn0fiublem  30767