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

Theorem sseq1i 3528
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 3525 . 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 1379    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  eqsstri  3534  syl5eqss  3548  ssab  3570  rabss  3577  uniiunlem  3588  prss  4181  prssg  4182  sstp  4191  tpss  4192  iunss  4366  pwtr  4700  pwssun  4786  cores2  5518  dffun2  5596  sbcfg  5727  fnsuppresOLD  6119  idref  6139  ovmptss  6861  fnsuppres  6924  ordgt0ge1  7144  omopthlem1  7301  trcl  8155  rankbnd  8282  rankbnd2  8283  rankc1  8284  dfac12a  8524  fin23lem34  8722  axdc2lem  8824  alephval2  8943  indpi  9281  fsuppmapnn0fiublem  12059  0ram  14390  mreacs  14906  lsslinds  18630  2ndcctbss  19719  xkoinjcn  19920  restmetu  20822  xrlimcnp  23023  mptelee  23871  ausisusgra  24028  frgraunss  24668  n4cyclfrgra  24691  shlesb1i  25977  mdsldmd1i  26923  csmdsymi  26926  dfon2lem3  28791  dfon2lem7  28795  sspred  28826  trpredmintr  28888  filnetlem4  29800  limccog  31162  cnvtrrel  36792  rp-imass  36796
  Copyright terms: Public domain W3C validator