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

Theorem sseq1i 2997
Description: An equality inference for the subclass relationship. (Contributed by NM, 18-Aug-1993.)
Hypothesis
Ref Expression
sseq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
sseq1i (𝐴𝐶𝐵𝐶)

Proof of Theorem sseq1i
StepHypRef Expression
1 sseq1i.1 . 2 𝐴 = 𝐵
2 sseq1 2994 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
31, 2ax-mp 7 1 (𝐴𝐶𝐵𝐶)
Colors of variables: wff set class
Syntax hints:  wb 102   = wceq 1259  wss 2945
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-11 1413  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-in 2952  df-ss 2959
This theorem is referenced by:  eqsstri  3003  syl5eqss  3017  ssab  3038  rabss  3045  uniiunlem  3056  prss  3548  prssg  3549  tpss  3557  iunss  3726  pwtr  3983  ordsucss  4258  elnn  4356  cores2  4861  dffun2  4940  funimaexglem  5010  idref  5424  ordgt0ge1  6049  prarloclemn  6655  bdeqsuc  10388  bj-omssind  10446
  Copyright terms: Public domain W3C validator