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

Theorem sseq1i 3592
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 3589 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 195   = wceq 1475  wss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554
This theorem is referenced by:  eqsstri  3598  syl5eqss  3612  ssab  3635  rabss  3642  uniiunlem  3653  prssg  4290  prssOLD  4292  sstp  4307  tpss  4308  iunss  4497  pwtr  4848  iunopeqop  4906  pwssun  4944  cores2  5565  sspred  5605  dffun2  5814  sbcfg  5956  idref  6403  ovmptss  7145  fnsuppres  7209  ordgt0ge1  7464  omopthlem1  7622  trcl  8487  rankbnd  8614  rankbnd2  8615  rankc1  8616  dfac12a  8853  fin23lem34  9051  axdc2lem  9153  alephval2  9273  indpi  9608  fsuppmapnn0fiublem  12651  0ram  15562  mreacs  16142  lsslinds  19989  2ndcctbss  21068  xkoinjcn  21300  restmetu  22185  xrlimcnp  24495  mptelee  25575  ausisusgra  25884  frgraunss  26522  n4cyclfrgra  26545  shlesb1i  27629  mdsldmd1i  28574  csmdsymi  28577  dfon2lem3  30934  dfon2lem7  30938  trpredmintr  30975  filnetlem4  31546  ptrecube  32579  poimirlem30  32609  undmrnresiss  36929  clcnvlem  36949  ss2iundf  36970  cnvtrrel  36981  brtrclfv2  37038  rp-imass  37085  dfhe3  37089  dffrege76  37253  iunssf  38290  ssabf  38308  rabssf  38334  ausgrusgrb  40395  nbuhgr2vtx1edgblem  40573  nbgrsym  40591  isuvtxa  40621  21wlkdlem6  41138  frcond1  41438  n4cyclfrgr  41461  setrec2  42241
  Copyright terms: Public domain W3C validator