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

Theorem sseq1i 3375
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 3372 . 2  |-  ( A  =  B  ->  ( A  C_  C  <->  B  C_  C
) )
31, 2ax-mp 5 1  |-  ( A 
C_  C  <->  B  C_  C
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1369    C_ wss 3323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337
This theorem is referenced by:  eqsstri  3381  syl5eqss  3395  ssab  3417  rabss  3424  uniiunlem  3435  prss  4022  prssg  4023  sstp  4032  tpss  4033  iunss  4206  pwtr  4540  pwssun  4622  cores2  5345  dffun2  5423  sbcfg  5552  fnsuppresOLD  5933  idref  5953  ovmptss  6649  fnsuppres  6711  ordgt0ge1  6929  omopthlem1  7086  trcl  7940  rankbnd  8067  rankbnd2  8068  rankc1  8069  dfac12a  8309  fin23lem34  8507  axdc2lem  8609  alephval2  8728  indpi  9068  0ram  14073  mreacs  14588  lsslinds  18240  2ndcctbss  19039  xkoinjcn  19240  restmetu  20142  xrlimcnp  22342  mptelee  23109  ausisusgra  23247  shlesb1i  24757  mdsldmd1i  25703  csmdsymi  25706  dfon2lem3  27567  dfon2lem7  27571  sspred  27602  trpredmintr  27664  filnetlem4  28573  frgraunss  30558  n4cyclfrgra  30581  fsuppmapnn0fiublem  30767
  Copyright terms: Public domain W3C validator