Theorem sseq1i 3950

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

Syntax hints:   ↔ wb 207   = wceq 1547   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ss 3907

This theorem is referenced by:  eqsstrid  3960  eqsstri  3968  ssab  4001  rabss  4008  uniiunlem  4025  prssg  4757  sstp  4774  tpss  4775  iunssfOLD  4980  iunssOLD  4982  pwtr  5398  iunopeqop  5469  iunopeqopOLD  5470  pwssun  5517  imadifssran  6109  cores2  6218  resssxp  6228  sspred  6268  sbcfg  6660  idref  7095  ovmptss  8039  fnsuppres  8138  frrlem7  8239  ordgt0ge1  8425  omopthlem1  8592  naddasslem1  8627  naddasslem2  8628  dmttrcl  9640  trcl  9647  rankbnd  9790  rankbnd2  9791  rankc1  9792  dfac12a  10069  fin23lem34  10266  alephval2  10493  indpi  10828  fsuppmapnn0fiublem  13950  prodeq1i  15879  0ram  16989  mreacs  17622  lsslinds  21813  2ndcctbss  23445  xkoinjcn  23677  restmetu  24560  xrlimcnp  26957  mpteleeOLD  28989  ausgrusgrb  29259  nbuhgr2vtx1edgblem  29445  nbgrsym  29457  isuvtx  29489  2wlkdlem6  30024  frcond1  30361  n4cyclfrgr  30386  shlesb1i  31482  mdsldmd1i  32427  csmdsymi  32430  tpssg  32632  lfuhgr  35353  2cycl2d  35374  dfon2lem3  36018  dfon2lem7  36022  cbvprodvw2  36482  filnetlem4  36616  ptrecube  37994  poimirlem30  38024  idinxpssinxp2  38698  cossssid2  38932  symrefref2  39021  redundeq1  39087  funALTVfun  39157  disjxrn  39220  omabs2  43784  undmrnresiss  44055  clcnvlem  44074  cnvtrrel  44121  brtrclfv2  44178  dfhe3  44226  dffrege76  44390  mnurndlem1  44732  ssabf  45554  rabssf  45573  imassmpt  45713  clnbgrsym  48336  sclnbgrelself  48346  setrec2  50192