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  4779  sstp  4795  tpss  4796  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  fnsuppres  8209  frrlem7  8311  ordgt0ge1  8502  omopthlem1  8669  naddasslem1  8705  naddasslem2  8706  dmttrcl  9723  trcl  9730  rankbnd  9886  rankbnd2  9887  rankc1  9888  setrec2  9978  dfac12a  10228  fin23lem34  10425  alephval2  10658  indpi  10993  fsuppmapnn0fiublem  14134  prodeq1i  16086  0ram  17199  mreacs  17833  lsslinds  22138  2ndcctbss  23775  xkoinjcn  24007  restmetu  24890  xrlimcnp  27297  mpteleeOLD  29474  lfuhgr  29727  ausgrusgrb  29747  nbuhgr2vtx1edgblem  29933  nbgrsym  29945  isuvtx  29977  2wlkdlem6  30521  frcond1  30868  n4cyclfrgr  30893  shlesb1i  31989  mdsldmd1i  32934  csmdsymi  32937  tpssg  33176  2cycl2d  35955  dfon2lem3  36590  dfon2lem7  36594  cbvprodvw2  37079  filnetlem4  37212  ptrecube  38582  poimirlem30  38612  idinxpssinxp2  39300  cossssid2  39534  symrefref2  39623  redundeq1  39689  funALTVfun  39759  disjxrn  39822  omabs2  44378  undmrnresiss  44648  clcnvlem  44667  cnvtrrel  44714  brtrclfv2  44771  dfhe3  44819  dffrege76  44983  mnurndlem1  45309  ssabf  46159  rabssf  46178  imassmpt  46318  clnbgrsym  48980  sclnbgrelself  48990