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

Step	Hyp	Ref	Expression
1		3sstr4g.1	. 2 |- ( ph -> A C_ B )
2		3sstr4g.2	. . 3 |- C = A
3		3sstr4g.3	. . 3 |- D = B
4	2, 3	sseq12i 3156	. 2 |- ( C C_ D <-> A C_ B )
5	1, 4	sylibr 133	1 |- ( ph -> C C_ D )

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