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

Theorem sseq1i 3372
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 3369 . 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 177    = wceq 1652    C_ wss 3320
This theorem is referenced by:  eqsstri  3378  syl5eqss  3392  ssab  3413  rabss  3420  uniiunlem  3431  prss  3952  prssg  3953  sstp  3963  tpss  3964  iunss  4132  pwtr  4416  pwssun  4489  cores2  5382  dffun2  5464  fnsuppres  5952  idref  5979  ovmptss  6428  ordgt0ge1  6741  omopthlem1  6898  trcl  7664  rankbnd  7794  rankbnd2  7795  rankc1  7796  dfac12a  8028  fin23lem34  8226  axdc2lem  8328  alephval2  8447  indpi  8784  0ram  13388  mreacs  13883  2ndcctbss  17518  xkoinjcn  17719  restmetu  18617  xrlimcnp  20807  ausisusgra  21380  shlesb1i  22888  mdsldmd1i  23834  csmdsymi  23837  dfon2lem3  25412  dfon2lem7  25416  sspred  25447  trpredmintr  25509  mptelee  25834  filnetlem4  26410  lsslinds  27278  frgraunss  28385  n4cyclfrgra  28408
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator