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

Theorem sseq1i 3202
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 3199 . 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 1623    C_ wss 3152
This theorem is referenced by:  eqsstri  3208  syl5eqss  3222  ssab  3243  rabss  3250  uniiunlem  3260  prss  3769  prssg  3770  sstp  3778  tpss  3779  iunss  3943  pwtr  4226  pwssun  4299  cores2  5185  dffun2  5265  fnsuppres  5732  idref  5759  ovmptss  6200  ordgt0ge1  6496  omopthlem1  6653  trcl  7410  rankbnd  7540  rankbnd2  7541  rankc1  7542  dfac12a  7774  fin23lem34  7972  axdc2lem  8074  alephval2  8194  indpi  8531  0ram  13067  mreacs  13560  2ndcctbss  17181  xkoinjcn  17381  xrlimcnp  20263  shlesb1i  21965  mdsldmd1i  22911  csmdsymi  22914  ballotth  23096  xrge00  23311  dfon2lem3  24141  dfon2lem7  24145  sspred  24174  trpredmintr  24234  mptelee  24523  toplat  25290  limptlimpr2lem2  25575  prismorcsetlemc  25917  filnetlem4  26330  lsslinds  27301
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator