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

Theorem sseqtrd 3105
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
sseqtrd.1  |-  ( ph  ->  A  C_  B )
sseqtrd.2  |-  ( ph  ->  B  =  C )
Assertion
Ref Expression
sseqtrd  |-  ( ph  ->  A  C_  C )

Proof of Theorem sseqtrd
StepHypRef Expression
1 sseqtrd.1 . 2  |-  ( ph  ->  A  C_  B )
2 sseqtrd.2 . . 3  |-  ( ph  ->  B  =  C )
32sseq2d 3097 . 2  |-  ( ph  ->  ( A  C_  B  <->  A 
C_  C ) )
41, 3mpbid 146 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1316    C_ wss 3041
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 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-11 1469  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-in 3047  df-ss 3054
This theorem is referenced by:  sseqtrrd  3106  fssdmd  5256  resasplitss  5272  nnaword2  6378  erssxp  6420  phpm  6727  ioodisj  9744  tgcl  12160  basgen  12176  bastop1  12179  bastop2  12180  clsss2  12225  topssnei  12258  cnntr  12321  txbasval  12363  neitx  12364  cnmpt1res  12392  cnmpt2res  12393  imasnopn  12395  hmeontr  12409  tgioo  12642  reldvg  12744  dvfvalap  12746  dvbss  12750  dvcnp2cntop  12759  dvaddxxbr  12761  dvmulxxbr  12762  dvcj  12769  nninfalllemn  13129
  Copyright terms: Public domain W3C validator