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

Theorem sseq1i 4012
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 4009 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 206   = wceq 1540  wss 3951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968
This theorem is referenced by:  eqsstrid  4022  eqsstri  4030  ssab  4064  rabss  4072  uniiunlem  4087  prssg  4819  sstp  4836  tpss  4837  iunssf  5044  iunss  5045  pwtr  5457  iunopeqop  5526  pwssun  5575  imadifssran  6171  cores2  6279  resssxp  6290  sspred  6330  dffun2OLDOLD  6573  sbcfg  6734  idref  7166  ovmptss  8118  fnsuppres  8216  frrlem7  8317  ordgt0ge1  8531  omopthlem1  8697  naddasslem1  8732  naddasslem2  8733  dmttrcl  9761  trcl  9768  rankbnd  9908  rankbnd2  9909  rankc1  9910  dfac12a  10189  fin23lem34  10386  axdc2lem  10488  alephval2  10612  indpi  10947  fsuppmapnn0fiublem  14031  prodeq1i  15952  0ram  17058  mreacs  17701  lsslinds  21851  2ndcctbss  23463  xkoinjcn  23695  restmetu  24583  xrlimcnp  27011  mptelee  28910  ausgrusgrb  29182  nbuhgr2vtx1edgblem  29368  nbgrsym  29380  isuvtx  29412  2wlkdlem6  29951  frcond1  30285  n4cyclfrgr  30310  shlesb1i  31405  mdsldmd1i  32350  csmdsymi  32353  lfuhgr  35123  2cycl2d  35144  dfon2lem3  35786  dfon2lem7  35790  cbvprodvw2  36248  filnetlem4  36382  ptrecube  37627  poimirlem30  37657  idinxpssinxp2  38319  cossssid2  38469  symrefref2  38564  redundeq1  38630  funALTVfun  38699  disjxrn  38747  omabs2  43345  undmrnresiss  43617  clcnvlem  43636  cnvtrrel  43683  brtrclfv2  43740  dfhe3  43788  dffrege76  43952  mnurndlem1  44300  ssabf  45105  rabssf  45124  imassmpt  45269  clnbgrsym  47824  sclnbgrelself  47834  setrec2  49214
  Copyright terms: Public domain W3C validator