Theorem sseq1i 3964

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

Syntax hints:   ↔ wb 208   = wceq 1559   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3921

This theorem is referenced by:  eqsstrid  3974  eqsstri  3982  ssab  4016  rabss  4023  uniiunlem  4040  prssg  4776  sstp  4793  tpss  4794  iunssfOLD  5000  iunssOLD  5002  pwtr  5418  iunopeqop  5489  iunopeqopOLD  5490  pwssun  5537  imadifssran  6133  cores2  6243  resssxp  6253  sspred  6293  sbcfg  6685  idref  7124  ovmptss  8067  fnsuppres  8166  frrlem7  8268  ordgt0ge1  8457  omopthlem1  8624  naddasslem1  8660  naddasslem2  8661  dmttrcl  9673  trcl  9680  rankbnd  9823  rankbnd2  9824  rankc1  9825  dfac12a  10102  fin23lem34  10300  alephval2  10527  indpi  10862  fsuppmapnn0fiublem  14000  prodeq1i  15929  0ram  17039  mreacs  17673  lsslinds  21863  2ndcctbss  23495  xkoinjcn  23727  restmetu  24610  xrlimcnp  27010  mpteleeOLD  29042  ausgrusgrb  29312  nbuhgr2vtx1edgblem  29498  nbgrsym  29510  isuvtx  29542  2wlkdlem6  30077  frcond1  30414  n4cyclfrgr  30439  shlesb1i  31535  mdsldmd1i  32480  csmdsymi  32483  tpssg  32685  lfuhgr  35432  2cycl2d  35453  dfon2lem3  36097  dfon2lem7  36101  cbvprodvw2  36571  filnetlem4  36705  ptrecube  38083  poimirlem30  38113  idinxpssinxp2  38787  cossssid2  39021  symrefref2  39110  redundeq1  39176  funALTVfun  39246  disjxrn  39309  omabs2  43873  undmrnresiss  44144  clcnvlem  44163  cnvtrrel  44210  brtrclfv2  44267  dfhe3  44315  dffrege76  44479  mnurndlem1  44821  ssabf  45642  rabssf  45661  imassmpt  45801  clnbgrsym  48424  sclnbgrelself  48434  setrec2  50280