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

Theorem eqsstri 3003
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 16-Jul-1995.)
Hypotheses
Ref Expression
eqsstr.1 𝐴 = 𝐵
eqsstr.2 𝐵𝐶
Assertion
Ref Expression
eqsstri 𝐴𝐶

Proof of Theorem eqsstri
StepHypRef Expression
1 eqsstr.2 . 2 𝐵𝐶
2 eqsstr.1 . . 3 𝐴 = 𝐵
32sseq1i 2997 . 2 (𝐴𝐶𝐵𝐶)
41, 3mpbir 138 1 𝐴𝐶
Colors of variables: wff set class
Syntax hints:   = 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:  eqsstr3i  3004  ssrab2  3053  rabssab  3055  difdifdirss  3335  opabss  3849  brab2ga  4443  relopabi  4491  dmopabss  4575  resss  4663  relres  4667  exse2  4727  rnin  4761  rnxpss  4782  cnvcnvss  4803  dmmptss  4845  fnres  5043  resasplitss  5097  fabexg  5105  f0  5108  ffvresb  5356  isoini2  5486  dmoprabss  5614  elmpt2cl  5726  tposssxp  5895  dftpos4  5909  smores  5938  smores2  5940  iordsmo  5943  swoer  6165  swoord1  6166  swoord2  6167  ecss  6178  ecopovsym  6233  ecopovtrn  6234  ecopover  6235  ecopovsymg  6236  ecopovtrng  6237  ecopoverg  6238  pinn  6465  niex  6468  ltrelpi  6480  dmaddpi  6481  dmmulpi  6482  enqex  6516  ltrelnq  6521  enq0ex  6595  ltrelpr  6661  enrex  6880  ltrelsr  6881  ltrelre  6967  ltrelxr  7139  lerelxr  7141  nn0ssre  8243  nn0ssz  8320  rpre  8687  cau3  9942  dvdszrcl  10113  dvdsflip  10163
  Copyright terms: Public domain W3C validator