Theorem sseq1i 3591

Description: An equality inference for the subclass relationship. (Contributed by NM, 18-Aug-1993.)

Hypothesis

Ref	Expression
sseq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
sseq1i	⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)

Proof of Theorem sseq1i

Step	Hyp	Ref	Expression
1		sseq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		sseq1 3588	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)

Syntax hints:   ↔ wb 194   = wceq 1474   ⊆ wss 3539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-in 3546  df-ss 3553

This theorem is referenced by:  eqsstri  3597  syl5eqss  3611  ssab  3634  rabss  3641  uniiunlem  3652  prssg  4289  prssOLD  4291  sstp  4302  tpss  4303  iunss  4491  pwtr  4841  pwssun  4933  cores2  5550  sspred  5590  dffun2  5799  sbcfg  5941  idref  6380  ovmptss  7122  fnsuppres  7186  ordgt0ge1  7441  omopthlem1  7599  trcl  8464  rankbnd  8591  rankbnd2  8592  rankc1  8593  dfac12a  8830  fin23lem34  9028  axdc2lem  9130  alephval2  9250  indpi  9585  fsuppmapnn0fiublem  12608  0ram  15510  mreacs  16090  lsslinds  19936  2ndcctbss  21015  xkoinjcn  21247  restmetu  22132  xrlimcnp  24439  mptelee  25520  ausisusgra  25677  frgraunss  26315  n4cyclfrgra  26338  shlesb1i  27422  mdsldmd1i  28367  csmdsymi  28370  dfon2lem3  30727  dfon2lem7  30731  trpredmintr  30768  filnetlem4  31339  ptrecube  32362  poimirlem30  32392  undmrnresiss  36712  clcnvlem  36732  ss2iundf  36753  cnvtrrel  36764  brtrclfv2  36821  rp-imass  36868  dfhe3  36872  dffrege76  37036  iunssf  38073  ssabf  38091  rabssf  38117  iunopeqop  40110  ausgrusgrb  40376  nbuhgr2vtx1edgblem  40554  nbgrsym  40572  isuvtxa  40602  21wlkdlem6  41119  frcond1  41419  n4cyclfrgr  41442