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

Theorem sseq1i 3993
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 3990 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 208   = wceq 1530  wss 3934
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-in 3941  df-ss 3950
This theorem is referenced by:  eqsstri  3999  eqsstrid  4013  ssab  4039  rabss  4046  uniiunlem  4059  prssg  4744  sstp  4759  tpss  4760  iunss  4960  pwtr  5336  iunopeqop  5402  pwssun  5448  cores2  6105  sspred  6149  dffun2  6358  sbcfg  6505  idref  6901  ovmptss  7780  fnsuppres  7849  ordgt0ge1  8114  omopthlem1  8274  trcl  9162  rankbnd  9289  rankbnd2  9290  rankc1  9291  dfac12a  9566  fin23lem34  9760  axdc2lem  9862  alephval2  9986  indpi  10321  fsuppmapnn0fiublem  13350  0ram  16348  mreacs  16921  lsslinds  20967  2ndcctbss  22055  xkoinjcn  22287  restmetu  23172  xrlimcnp  25538  mptelee  26673  ausgrusgrb  26942  nbuhgr2vtx1edgblem  27125  nbgrsym  27137  isuvtx  27169  2wlkdlem6  27702  frcond1  28037  n4cyclfrgr  28062  shlesb1i  29155  mdsldmd1i  30100  csmdsymi  30103  lfuhgr  32357  2cycl2d  32379  dfon2lem3  33023  dfon2lem7  33027  trpredmintr  33063  frrlem7  33122  filnetlem4  33722  ptrecube  34884  poimirlem30  34914  idinxpssinxp2  35567  cossssid2  35700  symrefref2  35791  redundeq1  35856  funALTVfun  35923  disjxrn  35969  undmrnresiss  39954  clcnvlem  39973  ss2iundf  39994  cnvtrrel  40005  brtrclfv2  40062  rp-imass  40107  dfhe3  40111  dffrege76  40275  mnurndlem1  40607  iunssf  41342  ssabf  41356  rabssf  41375  imassmpt  41526  setrec2  44788
  Copyright terms: Public domain W3C validator