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 186   = wceq 1407   C_ wss 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382

This theorem depends on definitions:  df-bi 187  df-an 371  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-in 3423  df-ss 3430

This theorem is referenced by:  eqsstri  3474  syl5eqss  3488  ssab  3511  rabss  3518  uniiunlem  3529  prss  4128  prssg  4129  sstp  4138  tpss  4139  iunss  4314  pwtr  4646  pwssun  4731  cores2  5338  sspred  5377  dffun2  5581  sbcfg  5714  fnsuppresOLD  6115  idref  6136  ovmptss  6867  fnsuppres  6932  ordgt0ge1  7186  omopthlem1  7343  trcl  8193  rankbnd  8320  rankbnd2  8321  rankc1  8322  dfac12a  8562  fin23lem34  8760  axdc2lem  8862  alephval2  8981  indpi  9317  fsuppmapnn0fiublem  12142  0ram  14749  mreacs  15274  lsslinds  19160  2ndcctbss  20250  xkoinjcn  20482  restmetu  21384  xrlimcnp  23626  mptelee  24627  ausisusgra  24784  frgraunss  25424  n4cyclfrgra  25447  shlesb1i  26731  mdsldmd1i  27676  csmdsymi  27679  dfon2lem3  30017  dfon2lem7  30021  trpredmintr  30058  filnetlem4  30622  ss2iundf  35651  cnvtrrel  35662  brtrclfv2  35719  rp-imass  35764  dfhe3  35768  dffrege76  35933