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

Theorem sseq1i 2946
 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𝐶B𝐶)

Proof of Theorem sseq1i
StepHypRef Expression
1 sseq1i.1 . 2 A = B
2 sseq1 2943 . 2 (A = B → (A𝐶B𝐶))
31, 2ax-mp 7 1 (A𝐶B𝐶)
 Colors of variables: wff set class Syntax hints:   ↔ wb 98   = wceq 1228   ⊆ wss 2894 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-11 1378  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004 This theorem depends on definitions:  df-bi 110  df-nf 1330  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-in 2901  df-ss 2908 This theorem is referenced by:  eqsstri  2952  syl5eqss  2966  ssab  2987  rabss  2994  uniiunlem  3005  prss  3494  prssg  3495  tpss  3503  iunss  3672  pwtr  3929  ordsucss  4180  elnn  4255  cores2  4760  dffun2  4839  funimaexglem  4908  idref  5321  ordgt0ge1  5933  prarloclemn  6353  bdeqsuc  7255  bj-omssind  7304
 Copyright terms: Public domain W3C validator