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  3736  prssg  3737  tpss  3745  iunss  3914  pwtr  4204  ordsucss  4488  elomssom  4589  cores2  5123  dffun2  5208  funimaexglem  5281  idref  5736  ordgt0ge1  6414  3nsssucpw1  7213  prarloclemn  7461  bdeqsuc  13916  bj-omssind  13970
  Copyright terms: Public domain W3C validator