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

Theorem eqsstri 3097
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 3091 . 2  |-  ( A 
C_  C  <->  B  C_  C
)
41, 3mpbir 145 1  |-  A  C_  C
Colors of variables: wff set class
Syntax hints:    = wceq 1314    C_ wss 3039
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-in 3045  df-ss 3052
This theorem is referenced by:  eqsstrri  3098  ssrab2  3150  rabssab  3152  difdifdirss  3415  opabss  3960  brab2ga  4582  relopabi  4633  dmopabss  4719  resss  4811  relres  4815  exse2  4881  rnin  4916  rnxpss  4938  cnvcnvss  4961  dmmptss  5003  cocnvss  5032  fnres  5207  resasplitss  5270  fabexg  5278  f0  5281  ffvresb  5549  isoini2  5686  dmoprabss  5819  elmpocl  5934  tposssxp  6112  dftpos4  6126  smores  6155  smores2  6157  iordsmo  6160  swoer  6423  swoord1  6424  swoord2  6425  ecss  6436  ecopovsym  6491  ecopovtrn  6492  ecopover  6493  ecopovsymg  6494  ecopovtrng  6495  ecopoverg  6496  sbthlem7  6817  caserel  6938  ctssdccl  6962  pinn  7081  niex  7084  ltrelpi  7096  dmaddpi  7097  dmmulpi  7098  enqex  7132  ltrelnq  7137  enq0ex  7211  ltrelpr  7277  enrex  7509  ltrelsr  7510  ltrelre  7605  axaddf  7640  axmulf  7641  ltrelxr  7789  lerelxr  7791  nn0ssre  8935  nn0ssz  9026  rpre  9399  fz1ssfz0  9848  cau3  10838  fsum3cvg3  11116  isumshft  11210  explecnv  11225  dvdszrcl  11405  dvdsflip  11456  infssuzcldc  11551  phimullem  11807  ctiunctlemuom  11855  structcnvcnv  11881  fvsetsid  11899  strleun  11954  dmtopon  12096  lmfval  12267  lmbrf  12290  cnconst2  12308  txuni2  12331  xmeter  12511  ivthinclemex  12695  dvrecap  12752
  Copyright terms: Public domain W3C validator