Theorem 3sstr4g 3646

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 3631	. 2 |- ( C C_ D <-> A C_ B )
5	1, 4	sylibr 224	1 |- ( ph -> C C_ D )

Syntax hints:   -> wi 4   = wceq 1483   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  rabss2  3685  unss2  3784  sslin  3839  intss  4498  ssopab2  5001  xpss12  5225  coss1  5277  coss2  5278  cnvss  5294  cnvssOLD  5295  rnss  5354  ssres  5424  ssres2  5425  imass1  5500  imass2  5501  predpredss  5686  ssoprab2  6711  ressuppss  7314  tposss  7353  onovuni  7439  ss2ixp  7921  fodomfi  8239  coss12d  13711  isumsplit  14572  isumrpcl  14575  cvgrat  14615  gsumzf1o  18313  gsumzmhm  18337  gsumzinv  18345  dsmmsubg  20087  qustgpopn  21923  metnrmlem2  22663  ovolsslem  23252  uniioombllem3  23353  ulmres  24142  xrlimcnp  24695  pntlemq  25290  cusgredg  26320  sspba  27582  shlej2i  28238  chpssati  29222  mptssALT  29474  bnj1408  31104  subfacp1lem6  31167  mthmpps  31479  qsss1  34053  aomclem4  37627  cotrclrcl  38034  fldc  42083  fldcALTV  42101