MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sseq1i Structured version   Visualization version   GIF version

Theorem sseq1i 3591
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
StepHypRef Expression
1 sseq1i.1 . 2 𝐴 = 𝐵
2 sseq1 3588 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 194   = wceq 1474  wss 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-in 3546  df-ss 3553
This theorem is referenced by:  eqsstri  3597  syl5eqss  3611  ssab  3634  rabss  3641  uniiunlem  3652  prssg  4289  prssOLD  4291  sstp  4302  tpss  4303  iunss  4491  pwtr  4841  pwssun  4933  cores2  5550  sspred  5590  dffun2  5799  sbcfg  5941  idref  6380  ovmptss  7122  fnsuppres  7186  ordgt0ge1  7441  omopthlem1  7599  trcl  8464  rankbnd  8591  rankbnd2  8592  rankc1  8593  dfac12a  8830  fin23lem34  9028  axdc2lem  9130  alephval2  9250  indpi  9585  fsuppmapnn0fiublem  12608  0ram  15510  mreacs  16090  lsslinds  19936  2ndcctbss  21015  xkoinjcn  21247  restmetu  22132  xrlimcnp  24439  mptelee  25520  ausisusgra  25677  frgraunss  26315  n4cyclfrgra  26338  shlesb1i  27422  mdsldmd1i  28367  csmdsymi  28370  dfon2lem3  30727  dfon2lem7  30731  trpredmintr  30768  filnetlem4  31339  ptrecube  32362  poimirlem30  32392  undmrnresiss  36712  clcnvlem  36732  ss2iundf  36753  cnvtrrel  36764  brtrclfv2  36821  rp-imass  36868  dfhe3  36872  dffrege76  37036  iunssf  38073  ssabf  38091  rabssf  38117  iunopeqop  40110  ausgrusgrb  40376  nbuhgr2vtx1edgblem  40554  nbgrsym  40572  isuvtxa  40602  21wlkdlem6  41119  frcond1  41419  n4cyclfrgr  41442
  Copyright terms: Public domain W3C validator