Theorem sseq1i 3958

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

Syntax hints:   ↔ wb 206   = wceq 1541   ⊆ wss 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3914

This theorem is referenced by:  eqsstrid  3968  eqsstri  3976  ssab  4011  rabss  4018  uniiunlem  4036  prssg  4770  sstp  4787  tpss  4788  iunssfOLD  4994  iunssOLD  4996  pwtr  5395  iunopeqop  5464  pwssun  5511  imadifssran  6104  cores2  6213  resssxp  6223  sspred  6263  sbcfg  6655  idref  7085  ovmptss  8029  fnsuppres  8127  frrlem7  8228  ordgt0ge1  8414  omopthlem1  8580  naddasslem1  8615  naddasslem2  8616  dmttrcl  9617  trcl  9624  rankbnd  9767  rankbnd2  9768  rankc1  9769  dfac12a  10046  fin23lem34  10243  alephval2  10469  indpi  10804  fsuppmapnn0fiublem  13903  prodeq1i  15829  0ram  16938  mreacs  17570  lsslinds  21774  2ndcctbss  23376  xkoinjcn  23608  restmetu  24491  xrlimcnp  26911  mpteleeOLD  28880  ausgrusgrb  29150  nbuhgr2vtx1edgblem  29336  nbgrsym  29348  isuvtx  29380  2wlkdlem6  29916  frcond1  30253  n4cyclfrgr  30278  shlesb1i  31373  mdsldmd1i  32318  csmdsymi  32321  tpssg  32524  lfuhgr  35169  2cycl2d  35190  dfon2lem3  35834  dfon2lem7  35838  cbvprodvw2  36298  filnetlem4  36432  ptrecube  37666  poimirlem30  37696  idinxpssinxp2  38362  cossssid2  38576  symrefref2  38665  redundeq1  38731  funALTVfun  38802  disjxrn  38850  omabs2  43430  undmrnresiss  43702  clcnvlem  43721  cnvtrrel  43768  brtrclfv2  43825  dfhe3  43873  dffrege76  44037  mnurndlem1  44379  ssabf  45202  rabssf  45221  imassmpt  45364  clnbgrsym  47943  sclnbgrelself  47953  setrec2  49801