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

Theorem sseq1i 3992
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 3989 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 207   = wceq 1528  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-in 3940  df-ss 3949
This theorem is referenced by:  eqsstri  3998  eqsstrid  4012  ssab  4038  rabss  4045  uniiunlem  4058  prssg  4744  sstp  4759  tpss  4760  iunss  4960  pwtr  5336  iunopeqop  5402  pwssun  5448  cores2  6105  sspred  6149  dffun2  6358  sbcfg  6505  idref  6900  ovmptss  7777  fnsuppres  7846  ordgt0ge1  8111  omopthlem1  8271  trcl  9158  rankbnd  9285  rankbnd2  9286  rankc1  9287  dfac12a  9562  fin23lem34  9756  axdc2lem  9858  alephval2  9982  indpi  10317  fsuppmapnn0fiublem  13346  0ram  16344  mreacs  16917  lsslinds  20903  2ndcctbss  21991  xkoinjcn  22223  restmetu  23107  xrlimcnp  25473  mptelee  26608  ausgrusgrb  26877  nbuhgr2vtx1edgblem  27060  nbgrsym  27072  isuvtx  27104  2wlkdlem6  27637  frcond1  27972  n4cyclfrgr  27997  shlesb1i  29090  mdsldmd1i  30035  csmdsymi  30038  lfuhgr  32261  2cycl2d  32283  dfon2lem3  32927  dfon2lem7  32931  trpredmintr  32967  frrlem7  33026  filnetlem4  33626  ptrecube  34773  poimirlem30  34803  idinxpssinxp2  35456  cossssid2  35588  symrefref2  35679  redundeq1  35744  funALTVfun  35811  disjxrn  35857  undmrnresiss  39842  clcnvlem  39861  ss2iundf  39882  cnvtrrel  39893  brtrclfv2  39950  rp-imass  39995  dfhe3  39999  dffrege76  40163  mnurndlem1  40494  iunssf  41229  ssabf  41243  rabssf  41262  imassmpt  41413  setrec2  44726
  Copyright terms: Public domain W3C validator