Theorem sseq1i 3962

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-ss 3919

This theorem is used by:  eqsstrid  3972  eqsstri  3980  ssab  4014  rabss  4021  uniiunlem  4038  prssg  4783  sstp  4799  tpss  4800  iunssfOLD  5006  iunssOLD  5008  pwtr  5431  iunopeqop  5502  iunopeqopOLD  5503  pwssun  5551  imadifssran  6201  imadifssranOLD  6202  cores2  6260  resssxp  6271  sspred  6312  sbcfg  6704  idref  7146  ovmptss  8094  fnsuppres  8193  frrlem7  8295  ordgt0ge1  8484  omopthlem1  8651  naddasslem1  8687  naddasslem2  8688  dmttrcl  9704  trcl  9711  rankbnd  9854  rankbnd2  9855  rankc1  9856  dfac12a  10155  fin23lem34  10352  alephval2  10585  indpi  10920  fsuppmapnn0fiublem  14058  prodeq1i  16009  0ram  17118  mreacs  17752  lsslinds  22050  2ndcctbss  23687  xkoinjcn  23919  restmetu  24802  xrlimcnp  27213  mpteleeOLD  29360  lfuhgr  29613  ausgrusgrb  29633  nbuhgr2vtx1edgblem  29819  nbgrsym  29831  isuvtx  29863  2wlkdlem6  30407  frcond1  30754  n4cyclfrgr  30779  shlesb1i  31875  mdsldmd1i  32820  csmdsymi  32823  tpssg  33020  2cycl2d  35734  dfon2lem3  36370  dfon2lem7  36374  cbvprodvw2  36875  filnetlem4  37008  ptrecube  38377  poimirlem30  38407  idinxpssinxp2  39080  cossssid2  39314  symrefref2  39403  redundeq1  39469  funALTVfun  39539  disjxrn  39602  omabs2  44181  undmrnresiss  44452  clcnvlem  44471  cnvtrrel  44518  brtrclfv2  44575  dfhe3  44623  dffrege76  44787  mnurndlem1  45113  ssabf  45940  rabssf  45959  imassmpt  46099  clnbgrsym  48762  sclnbgrelself  48772  setrec2  50629