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

Theorem sseq1i 4008
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 4005 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1542  wss 3946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3953  df-ss 3963
This theorem is referenced by:  eqsstri  4014  eqsstrid  4028  ssab  4056  rabss  4067  uniiunlem  4082  prssg  4820  sstp  4835  tpss  4836  iunssf  5045  iunss  5046  pwtr  5450  iunopeqop  5519  pwssun  5569  cores2  6254  resssxp  6265  sspred  6305  dffun2OLDOLD  6551  sbcfg  6711  idref  7138  ovmptss  8073  fnsuppres  8170  frrlem7  8271  ordgt0ge1  8487  omopthlem1  8653  naddasslem1  8688  naddasslem2  8689  dmttrcl  9711  trcl  9718  rankbnd  9858  rankbnd2  9859  rankc1  9860  dfac12a  10138  fin23lem34  10336  axdc2lem  10438  alephval2  10562  indpi  10897  fsuppmapnn0fiublem  13950  0ram  16948  mreacs  17597  lsslinds  21369  2ndcctbss  22940  xkoinjcn  23172  restmetu  24060  xrlimcnp  26452  mptelee  28132  ausgrusgrb  28404  nbuhgr2vtx1edgblem  28587  nbgrsym  28599  isuvtx  28631  2wlkdlem6  29164  frcond1  29498  n4cyclfrgr  29523  shlesb1i  30616  mdsldmd1i  31561  csmdsymi  31564  lfuhgr  34045  2cycl2d  34067  dfon2lem3  34694  dfon2lem7  34698  filnetlem4  35203  ptrecube  36425  poimirlem30  36455  idinxpssinxp2  37124  cossssid2  37275  symrefref2  37370  redundeq1  37436  funALTVfun  37505  disjxrn  37553  omabs2  42014  undmrnresiss  42287  clcnvlem  42306  cnvtrrel  42353  brtrclfv2  42410  dfhe3  42458  dffrege76  42622  mnurndlem1  42972  ssabf  43721  rabssf  43740  imassmpt  43901  setrec2  47641
  Copyright terms: Public domain W3C validator