Theorem sseq1i 3936

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896

This theorem is used by:  eqsstrid  3946  eqsstri  3954  ssab  3988  rabss  3995  uniiunlem  4012  prssg  4774  sstp  4790  tpss  4791  iunssfOLD  5001  iunssOLD  5003  pwtr  5419  iunopeqop  5493  iunopeqopOLD  5494  pwssun  5542  cnvimassrndm  6078  imadifssranOLD  6202  imadifssranOLDOLD  6203  cores2  6261  resssxp  6272  sspred  6313  sbcfg  6707  idref  7149  ovmptss  8104  ovmptssOLD  8105  fnsuppres  8211  frrlem7  8313  ordgt0ge1  8504  omopthlem1  8671  naddasslem1  8707  naddasslem2  8708  dmttrcl  9725  trcl  9732  rankbnd  9888  rankbnd2  9889  rankc1  9890  setrec2  9980  dfac12a  10230  fin23lem34  10427  alephval2  10660  indpi  10995  fsuppmapnn0fiublem  14136  prodeq1i  16090  0ram  17203  mreacs  17837  lsslinds  22142  2ndcctbss  23779  xkoinjcn  24011  restmetu  24894  xrlimcnp  27301  mpteleeOLD  29478  lfuhgr  29731  ausgrusgrb  29751  nbuhgr2vtx1edgblem  29937  nbgrsym  29949  isuvtx  29981  2wlkdlem6  30525  frcond1  30872  n4cyclfrgr  30897  shlesb1i  31993  mdsldmd1i  32938  csmdsymi  32941  tpssg  33180  2cycl2d  35988  dfon2lem3  36639  dfon2lem7  36643  cbvprodvw2  37128  filnetlem4  37261  ptrecube  38631  poimirlem30  38661  idinxpssinxp2  39349  cossssid2  39583  symrefref2  39672  redundeq1  39738  funALTVfun  39808  disjxrn  39871  omabs2  44427  undmrnresiss  44697  clcnvlem  44716  cnvtrrel  44763  brtrclfv2  44820  dfhe3  44868  dffrege76  45032  mnurndlem1  45358  ssabf  46208  rabssf  46227  imassmpt  46367  clnbgrsym  49029  sclnbgrelself  49039