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

Theorem sseq1i 3527
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 3524 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  =wceq 1395  C_wss 3475
This theorem is referenced by:  eqsstri  3533  syl5eqss  3547  ssab  3569  rabss  3576  uniiunlem  3587  prss  4184  prssg  4185  sstp  4194  tpss  4195  iunss  4371  pwtr  4705  pwssun  4791  cores2  5525  dffun2  5603  sbcfg  5734  fnsuppresOLD  6131  idref  6153  ovmptss  6881  fnsuppres  6946  ordgt0ge1  7166  omopthlem1  7323  trcl  8180  rankbnd  8307  rankbnd2  8308  rankc1  8309  dfac12a  8549  fin23lem34  8747  axdc2lem  8849  alephval2  8968  indpi  9306  fsuppmapnn0fiublem  12096  0ram  14538  mreacs  15055  lsslinds  18866  2ndcctbss  19956  xkoinjcn  20188  restmetu  21090  xrlimcnp  23298  mptelee  24198  ausisusgra  24355  frgraunss  24995  n4cyclfrgra  25018  shlesb1i  26304  mdsldmd1i  27250  csmdsymi  27253  dfon2lem3  29217  dfon2lem7  29221  sspred  29252  trpredmintr  29314  filnetlem4  30199  cnvtrrel  37782  rp-imass  37795  dfhe3  37799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator