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

Theorem sseq1i 3215
Description: An equality inference for the subclass relationship. (Contributed by NM, 18-Aug-1993.)
Hypothesis
Ref Expression
sseq1i.1  |-  A  =  B
Assertion
Ref Expression
sseq1i  |-  ( A 
C_  C  <->  B  C_  C
)

Proof of Theorem sseq1i
StepHypRef Expression
1 sseq1i.1 . 2  |-  A  =  B
2 sseq1 3212 . 2  |-  ( A  =  B  ->  ( A  C_  C  <->  B  C_  C
) )
31, 2ax-mp 8 1  |-  ( A 
C_  C  <->  B  C_  C
)
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1632    C_ wss 3165
This theorem is referenced by:  eqsstri  3221  syl5eqss  3235  ssab  3256  rabss  3263  uniiunlem  3273  prss  3785  prssg  3786  sstp  3794  tpss  3795  iunss  3959  pwtr  4242  pwssun  4315  cores2  5201  dffun2  5281  fnsuppres  5748  idref  5775  ovmptss  6216  ordgt0ge1  6512  omopthlem1  6669  trcl  7426  rankbnd  7556  rankbnd2  7557  rankc1  7558  dfac12a  7790  fin23lem34  7988  axdc2lem  8090  alephval2  8210  indpi  8547  0ram  13083  mreacs  13576  2ndcctbss  17197  xkoinjcn  17397  xrlimcnp  20279  shlesb1i  21981  mdsldmd1i  22927  csmdsymi  22930  ballotth  23112  xrge00  23326  dfon2lem3  24212  dfon2lem7  24216  sspred  24245  trpredmintr  24305  mptelee  24595  toplat  25393  limptlimpr2lem2  25678  prismorcsetlemc  26020  filnetlem4  26433  lsslinds  27404  n4cyclfrgra  28440
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator