Theorem sseq1i 3528

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 3525	. 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 1379   C_ wss 3476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490

This theorem is referenced by:  eqsstri  3534  syl5eqss  3548  ssab  3570  rabss  3577  uniiunlem  3588  prss  4181  prssg  4182  sstp  4191  tpss  4192  iunss  4366  pwtr  4700  pwssun  4786  cores2  5518  dffun2  5596  sbcfg  5727  fnsuppresOLD  6119  idref  6139  ovmptss  6861  fnsuppres  6924  ordgt0ge1  7144  omopthlem1  7301  trcl  8155  rankbnd  8282  rankbnd2  8283  rankc1  8284  dfac12a  8524  fin23lem34  8722  axdc2lem  8824  alephval2  8943  indpi  9281  fsuppmapnn0fiublem  12059  0ram  14390  mreacs  14906  lsslinds  18630  2ndcctbss  19719  xkoinjcn  19920  restmetu  20822  xrlimcnp  23023  mptelee  23871  ausisusgra  24028  frgraunss  24668  n4cyclfrgra  24691  shlesb1i  25977  mdsldmd1i  26923  csmdsymi  26926  dfon2lem3  28791  dfon2lem7  28795  sspred  28826  trpredmintr  28888  filnetlem4  29800  limccog  31162  cnvtrrel  36792  rp-imass  36796