Theorem sseq1i 3951

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

Syntax hints:   ↔ wb 206   = wceq 1542   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907

This theorem is referenced by:  eqsstrid  3961  eqsstri  3969  ssab  4004  rabss  4011  uniiunlem  4028  prssg  4763  sstp  4780  tpss  4781  iunssfOLD  4987  iunssOLD  4989  pwtr  5399  iunopeqop  5469  pwssun  5516  imadifssran  6109  cores2  6218  resssxp  6228  sspred  6268  sbcfg  6660  idref  7093  ovmptss  8036  fnsuppres  8134  frrlem7  8235  ordgt0ge1  8421  omopthlem1  8588  naddasslem1  8623  naddasslem2  8624  dmttrcl  9633  trcl  9640  rankbnd  9783  rankbnd2  9784  rankc1  9785  dfac12a  10062  fin23lem34  10259  alephval2  10486  indpi  10821  fsuppmapnn0fiublem  13943  prodeq1i  15872  0ram  16982  mreacs  17615  lsslinds  21821  2ndcctbss  23430  xkoinjcn  23662  restmetu  24545  xrlimcnp  26945  mpteleeOLD  28978  ausgrusgrb  29248  nbuhgr2vtx1edgblem  29434  nbgrsym  29446  isuvtx  29478  2wlkdlem6  30014  frcond1  30351  n4cyclfrgr  30376  shlesb1i  31472  mdsldmd1i  32417  csmdsymi  32420  tpssg  32622  lfuhgr  35316  2cycl2d  35337  dfon2lem3  35981  dfon2lem7  35985  cbvprodvw2  36445  filnetlem4  36579  ptrecube  37955  poimirlem30  37985  idinxpssinxp2  38659  cossssid2  38893  symrefref2  38982  redundeq1  39048  funALTVfun  39118  disjxrn  39181  omabs2  43778  undmrnresiss  44049  clcnvlem  44068  cnvtrrel  44115  brtrclfv2  44172  dfhe3  44220  dffrege76  44384  mnurndlem1  44726  ssabf  45548  rabssf  45567  imassmpt  45709  clnbgrsym  48326  sclnbgrelself  48336  setrec2  50182