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

Theorem 3sstr4g 3171
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 3156 . 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 1335    C_ wss 3102
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 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139
This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-in 3108  df-ss 3115
This theorem is referenced by:  rabss2  3211  unss2  3278  sslin  3333  ssopab2  4235  xpss12  4693  coss1  4741  coss2  4742  cnvss  4759  rnss  4816  ssres  4892  ssres2  4893  imass1  4961  imass2  4962  imadif  5250  imain  5252  ssoprab2  5877  suppssfv  6028  suppssov1  6029  tposss  6193  ss2ixp  6656  isumsplit  11388  isumrpcl  11391
  Copyright terms: Public domain W3C validator