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 206   = wceq 1540   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3922

This theorem is referenced by:  eqsstrid  3976  eqsstri  3984  ssab  4018  rabss  4025  uniiunlem  4040  prssg  4773  sstp  4790  tpss  4791  iunssf  4996  iunss  4997  pwtr  5399  iunopeqop  5468  pwssun  5515  imadifssran  6104  cores2  6212  resssxp  6222  sspred  6262  sbcfg  6654  idref  7084  ovmptss  8033  fnsuppres  8131  frrlem7  8232  ordgt0ge1  8418  omopthlem1  8584  naddasslem1  8619  naddasslem2  8620  dmttrcl  9636  trcl  9643  rankbnd  9783  rankbnd2  9784  rankc1  9785  dfac12a  10062  fin23lem34  10259  axdc2lem  10361  alephval2  10485  indpi  10820  fsuppmapnn0fiublem  13915  prodeq1i  15841  0ram  16950  mreacs  17582  lsslinds  21756  2ndcctbss  23358  xkoinjcn  23590  restmetu  24474  xrlimcnp  26894  mptelee  28858  ausgrusgrb  29128  nbuhgr2vtx1edgblem  29314  nbgrsym  29326  isuvtx  29358  2wlkdlem6  29894  frcond1  30228  n4cyclfrgr  30253  shlesb1i  31348  mdsldmd1i  32293  csmdsymi  32296  tpssg  32499  lfuhgr  35090  2cycl2d  35111  dfon2lem3  35758  dfon2lem7  35762  cbvprodvw2  36220  filnetlem4  36354  ptrecube  37599  poimirlem30  37629  idinxpssinxp2  38291  cossssid2  38444  symrefref2  38539  redundeq1  38605  funALTVfun  38675  disjxrn  38723  omabs2  43305  undmrnresiss  43577  clcnvlem  43596  cnvtrrel  43643  brtrclfv2  43700  dfhe3  43748  dffrege76  43912  mnurndlem1  44254  ssabf  45078  rabssf  45097  imassmpt  45240  clnbgrsym  47823  sclnbgrelself  47833  setrec2  49681