ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sseq1i Unicode version

Theorem sseq1i 3173
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 3170 . 2  |-  ( A  =  B  ->  ( A  C_  C  <->  B  C_  C
) )
31, 2ax-mp 5 1  |-  ( A 
C_  C  <->  B  C_  C
)
Colors of variables: wff set class
Syntax hints:    <-> wb 104    = wceq 1348    C_ wss 3121
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134
This theorem is referenced by:  eqsstri  3179  eqsstrid  3193  ssab  3217  rabss  3224  uniiunlem  3236  prss  3734  prssg  3735  tpss  3743  iunss  3912  pwtr  4202  ordsucss  4486  elomssom  4587  cores2  5121  dffun2  5206  funimaexglem  5279  idref  5733  ordgt0ge1  6411  3nsssucpw1  7200  prarloclemn  7448  bdeqsuc  13876  bj-omssind  13930
  Copyright terms: Public domain W3C validator