Theorem sseq1i 4024

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

Syntax hints:   ↔ wb 206   = wceq 1537   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-ss 3980

This theorem is referenced by:  eqsstri  4030  eqsstrid  4044  ssab  4074  rabss  4082  uniiunlem  4097  prssg  4824  sstp  4841  tpss  4842  iunssf  5049  iunss  5050  pwtr  5463  iunopeqop  5531  pwssun  5580  cores2  6281  resssxp  6292  sspred  6332  dffun2OLDOLD  6575  sbcfg  6735  idref  7166  ovmptss  8117  fnsuppres  8215  frrlem7  8316  ordgt0ge1  8530  omopthlem1  8696  naddasslem1  8731  naddasslem2  8732  dmttrcl  9759  trcl  9766  rankbnd  9906  rankbnd2  9907  rankc1  9908  dfac12a  10187  fin23lem34  10384  axdc2lem  10486  alephval2  10610  indpi  10945  fsuppmapnn0fiublem  14028  prodeq1i  15949  0ram  17054  mreacs  17703  lsslinds  21869  2ndcctbss  23479  xkoinjcn  23711  restmetu  24599  xrlimcnp  27026  mptelee  28925  ausgrusgrb  29197  nbuhgr2vtx1edgblem  29383  nbgrsym  29395  isuvtx  29427  2wlkdlem6  29961  frcond1  30295  n4cyclfrgr  30320  shlesb1i  31415  mdsldmd1i  32360  csmdsymi  32363  lfuhgr  35102  2cycl2d  35124  dfon2lem3  35767  dfon2lem7  35771  cbvprodvw2  36230  filnetlem4  36364  ptrecube  37607  poimirlem30  37637  idinxpssinxp2  38300  cossssid2  38450  symrefref2  38545  redundeq1  38611  funALTVfun  38680  disjxrn  38728  omabs2  43322  undmrnresiss  43594  clcnvlem  43613  cnvtrrel  43660  brtrclfv2  43717  dfhe3  43765  dffrege76  43929  mnurndlem1  44277  ssabf  45040  rabssf  45059  imassmpt  45208  clnbgrsym  47762  sclnbgrelself  47772  setrec2  48926