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

Theorem eqsstri 3054
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 16-Jul-1995.)
Hypotheses
Ref Expression
eqsstr.1  |-  A  =  B
eqsstr.2  |-  B  C_  C
Assertion
Ref Expression
eqsstri  |-  A  C_  C

Proof of Theorem eqsstri
StepHypRef Expression
1 eqsstr.2 . 2  |-  B  C_  C
2 eqsstr.1 . . 3  |-  A  =  B
32sseq1i 3048 . 2  |-  ( A 
C_  C  <->  B  C_  C
)
41, 3mpbir 144 1  |-  A  C_  C
Colors of variables: wff set class
Syntax hints:    = wceq 1289    C_ wss 2997
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-11 1442  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-in 3003  df-ss 3010
This theorem is referenced by:  eqsstr3i  3055  ssrab2  3104  rabssab  3106  difdifdirss  3363  opabss  3894  brab2ga  4501  relopabi  4551  dmopabss  4636  resss  4724  relres  4728  exse2  4793  rnin  4828  rnxpss  4849  cnvcnvss  4872  dmmptss  4914  cocnvss  4943  fnres  5116  resasplitss  5174  fabexg  5182  f0  5185  ffvresb  5445  isoini2  5580  dmoprabss  5712  elmpt2cl  5824  tposssxp  5996  dftpos4  6010  smores  6039  smores2  6041  iordsmo  6044  swoer  6300  swoord1  6301  swoord2  6302  ecss  6313  ecopovsym  6368  ecopovtrn  6369  ecopover  6370  ecopovsymg  6371  ecopovtrng  6372  ecopoverg  6373  sbthlem7  6651  djuun  6739  caserel  6757  pinn  6847  niex  6850  ltrelpi  6862  dmaddpi  6863  dmmulpi  6864  enqex  6898  ltrelnq  6903  enq0ex  6977  ltrelpr  7043  enrex  7262  ltrelsr  7263  ltrelre  7349  ltrelxr  7526  lerelxr  7528  nn0ssre  8647  nn0ssz  8738  rpre  9109  cau3  10513  fisumcvg3  10752  isumshft  10846  explecnv  10860  dvdszrcl  10883  dvdsflip  10934  infssuzcldc  11029  phimullem  11283
  Copyright terms: Public domain W3C validator