Theorem sseq1i 3967

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

Syntax hints:   ↔ wb 209   = wceq 1563   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ss 3924

This theorem is referenced by:  eqsstrid  3977  eqsstri  3985  ssab  4019  rabss  4026  uniiunlem  4043  prssg  4780  sstp  4797  tpss  4798  iunssfOLD  5004  iunssOLD  5006  pwtr  5424  iunopeqop  5495  iunopeqopOLD  5496  pwssun  5544  imadifssran  6140  cores2  6251  resssxp  6261  sspred  6301  sbcfg  6693  idref  7132  ovmptss  8076  fnsuppres  8175  frrlem7  8277  ordgt0ge1  8466  omopthlem1  8633  naddasslem1  8669  naddasslem2  8670  dmttrcl  9678  trcl  9685  rankbnd  9828  rankbnd2  9829  rankc1  9830  dfac12a  10120  fin23lem34  10318  alephval2  10545  indpi  10880  fsuppmapnn0fiublem  14017  prodeq1i  15960  0ram  17070  mreacs  17704  lsslinds  21941  2ndcctbss  23573  xkoinjcn  23805  restmetu  24688  xrlimcnp  27091  mpteleeOLD  29154  ausgrusgrb  29424  nbuhgr2vtx1edgblem  29610  nbgrsym  29622  isuvtx  29654  2wlkdlem6  30189  frcond1  30526  n4cyclfrgr  30551  shlesb1i  31647  mdsldmd1i  32592  csmdsymi  32595  tpssg  32793  lfuhgr  35481  2cycl2d  35502  dfon2lem3  36146  dfon2lem7  36150  cbvprodvw2  36620  filnetlem4  36754  ptrecube  38131  poimirlem30  38161  idinxpssinxp2  38835  cossssid2  39069  symrefref2  39158  redundeq1  39224  funALTVfun  39294  disjxrn  39357  omabs2  43921  undmrnresiss  44192  clcnvlem  44211  cnvtrrel  44258  brtrclfv2  44315  dfhe3  44363  dffrege76  44527  mnurndlem1  44855  ssabf  45676  rabssf  45695  imassmpt  45835  clnbgrsym  48458  sclnbgrelself  48468  setrec2  50324