Theorem sseq1i 3966

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 3963	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)

Syntax hints:   ↔ wb 209   = wceq 1570   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3923

This theorem is referenced by:  eqsstrid  3976  eqsstri  3984  ssab  4018  rabss  4025  uniiunlem  4042  prssg  4786  sstp  4802  tpss  4803  iunssfOLD  5009  iunssOLD  5011  pwtr  5435  iunopeqop  5506  iunopeqopOLD  5507  pwssun  5555  imadifssran  6204  imadifssranOLD  6205  cores2  6263  resssxp  6273  sspred  6313  sbcfg  6705  idref  7144  ovmptss  8089  fnsuppres  8188  frrlem7  8290  ordgt0ge1  8479  omopthlem1  8646  naddasslem1  8682  naddasslem2  8683  dmttrcl  9691  trcl  9698  rankbnd  9841  rankbnd2  9842  rankc1  9843  dfac12a  10133  fin23lem34  10331  alephval2  10558  indpi  10893  fsuppmapnn0fiublem  14028  prodeq1i  15972  0ram  17081  mreacs  17715  lsslinds  21962  2ndcctbss  23593  xkoinjcn  23825  restmetu  24708  xrlimcnp  27111  mpteleeOLD  29223  ausgrusgrb  29493  nbuhgr2vtx1edgblem  29679  nbgrsym  29691  isuvtx  29723  2wlkdlem6  30258  frcond1  30595  n4cyclfrgr  30620  shlesb1i  31716  mdsldmd1i  32661  csmdsymi  32664  tpssg  32861  lfuhgr  35588  2cycl2d  35609  dfon2lem3  36253  dfon2lem7  36257  cbvprodvw2  36737  filnetlem4  36870  ptrecube  38249  poimirlem30  38279  idinxpssinxp2  38951  cossssid2  39185  symrefref2  39274  redundeq1  39340  funALTVfun  39410  disjxrn  39473  omabs2  44039  undmrnresiss  44310  clcnvlem  44329  cnvtrrel  44376  brtrclfv2  44433  dfhe3  44481  dffrege76  44645  mnurndlem1  44971  ssabf  45798  rabssf  45817  imassmpt  45957  clnbgrsym  48580  sclnbgrelself  48590  setrec2  50450