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

Theorem sseqtr4i 3060
 Description: Substitution of equality into a subclass relationship. (Contributed by NM, 4-Apr-1995.)
Hypotheses
Ref Expression
sseqtr4.1 𝐴𝐵
sseqtr4.2 𝐶 = 𝐵
Assertion
Ref Expression
sseqtr4i 𝐴𝐶

Proof of Theorem sseqtr4i
StepHypRef Expression
1 sseqtr4.1 . 2 𝐴𝐵
2 sseqtr4.2 . . 3 𝐶 = 𝐵
32eqcomi 2093 . 2 𝐵 = 𝐶
41, 3sseqtri 3059 1 𝐴𝐶
 Colors of variables: wff set class Syntax hints:   = wceq 1290   ⊆ wss 3000 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-11 1443  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071 This theorem depends on definitions:  df-bi 116  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-in 3006  df-ss 3013 This theorem is referenced by:  eqimss2i  3082  difdif2ss  3257  snsspr1  3591  snsspr2  3592  snsstp1  3593  snsstp2  3594  snsstp3  3595  prsstp12  3596  prsstp13  3597  prsstp23  3598  iunxdif2  3784  pwpwssunieq  3823  sssucid  4251  opabssxp  4525  dmresi  4780  cnvimass  4808  ssrnres  4886  cnvcnv  4896  cnvssrndm  4965  dmmpt2ssx  5983  tfrcllemssrecs  6131  sucinc  6220  mapex  6425  exmidpw  6678  casefun  6830  djufun  6839  ressxr  7585  ltrelxr  7601  nnssnn0  8730  un0addcl  8760  un0mulcl  8761  nn0ssxnn0  8793  fzssnn  9536  fzossnn0  9640  isumclim3  10871  isprm3  11432  phimullem  11533  tgvalex  11804
 Copyright terms: Public domain W3C validator