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

Theorem 3sstr4g 3190
Description: Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
Hypotheses
Ref Expression
3sstr4g.1  |-  ( ph  ->  A  C_  B )
3sstr4g.2  |-  C  =  A
3sstr4g.3  |-  D  =  B
Assertion
Ref Expression
3sstr4g  |-  ( ph  ->  C  C_  D )

Proof of Theorem 3sstr4g
StepHypRef Expression
1 3sstr4g.1 . 2  |-  ( ph  ->  A  C_  B )
2 3sstr4g.2 . . 3  |-  C  =  A
3 3sstr4g.3 . . 3  |-  D  =  B
42, 3sseq12i 3175 . 2  |-  ( C 
C_  D  <->  A  C_  B
)
51, 4sylibr 133 1  |-  ( ph  ->  C  C_  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1348    C_ wss 3121
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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134
This theorem is referenced by:  rabss2  3230  unss2  3298  sslin  3353  ssopab2  4260  xpss12  4718  coss1  4766  coss2  4767  cnvss  4784  rnss  4841  ssres  4917  ssres2  4918  imass1  4986  imass2  4987  imadif  5278  imain  5280  ssoprab2  5909  suppssfv  6057  suppssov1  6058  tposss  6225  ss2ixp  6689  isumsplit  11454  isumrpcl  11457
  Copyright terms: Public domain W3C validator