Theorem sseq1i 3959

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

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

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 2123  ax-ext 2705

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

This theorem is referenced by:  eqsstrid  3969  eqsstri  3977  ssab  4012  rabss  4019  uniiunlem  4036  prssg  4770  sstp  4787  tpss  4788  iunssfOLD  4994  iunssOLD  4996  pwtr  5395  iunopeqop  5464  pwssun  5511  imadifssran  6103  cores2  6212  resssxp  6222  sspred  6262  sbcfg  6654  idref  7085  ovmptss  8029  fnsuppres  8127  frrlem7  8228  ordgt0ge1  8414  omopthlem1  8580  naddasslem1  8615  naddasslem2  8616  dmttrcl  9618  trcl  9625  rankbnd  9768  rankbnd2  9769  rankc1  9770  dfac12a  10047  fin23lem34  10244  alephval2  10470  indpi  10805  fsuppmapnn0fiublem  13899  prodeq1i  15825  0ram  16934  mreacs  17566  lsslinds  21770  2ndcctbss  23371  xkoinjcn  23603  restmetu  24486  xrlimcnp  26906  mpteleeOLD  28875  ausgrusgrb  29145  nbuhgr2vtx1edgblem  29331  nbgrsym  29343  isuvtx  29375  2wlkdlem6  29911  frcond1  30248  n4cyclfrgr  30273  shlesb1i  31368  mdsldmd1i  32313  csmdsymi  32316  tpssg  32519  lfuhgr  35183  2cycl2d  35204  dfon2lem3  35848  dfon2lem7  35852  cbvprodvw2  36312  filnetlem4  36446  ptrecube  37680  poimirlem30  37710  idinxpssinxp2  38376  cossssid2  38590  symrefref2  38679  redundeq1  38745  funALTVfun  38816  disjxrn  38864  omabs2  43449  undmrnresiss  43721  clcnvlem  43740  cnvtrrel  43787  brtrclfv2  43844  dfhe3  43892  dffrege76  44056  mnurndlem1  44398  ssabf  45221  rabssf  45240  imassmpt  45383  clnbgrsym  47962  sclnbgrelself  47972  setrec2  49820