Theorem 3sstr4g 4000

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	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
3sstr4g.2	⊢ 𝐶 = 𝐴
3sstr4g.3	⊢ 𝐷 = 𝐵

Assertion

Ref	Expression
3sstr4g	⊢ (𝜑 → 𝐶 ⊆ 𝐷)

Proof of Theorem 3sstr4g

Step	Hyp	Ref	Expression
1		3sstr4g.2	. . 3 ⊢ 𝐶 = 𝐴
2		3sstr4g.1	. . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
3	1, 2	eqsstrid 3985	. 2 ⊢ (𝜑 → 𝐶 ⊆ 𝐵)
4		3sstr4g.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	sseqtrrdi 3988	1 ⊢ (𝜑 → 𝐶 ⊆ 𝐷)

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931

This theorem is referenced by:  rabss2  4041  unss2  4150  sslin  4206  intss  4933  ssopab2  5506  xpss12  5653  coss1  5819  coss2  5820  cnvss  5836  rnss  5903  ssres  5974  ssres2  5975  imass1  6072  imass2  6073  predpredss  6281  predrelss  6310  ssoprab2  7457  ressuppss  8162  tposss  8206  onovuni  8311  ss2ixp  8883  fodomfi  9261  fodomfiOLD  9281  coss12d  14938  isumsplit  15806  isumrpcl  15809  cvgrat  15849  gsumzf1o  19842  gsumzmhm  19867  gsumzinv  19875  fldc  20693  dsmmsubg  21652  qustgpopn  24007  metnrmlem2  24749  ovolsslem  25385  uniioombllem3  25486  ulmres  26297  xrlimcnp  26878  pntlemq  27512  cusgredg  29351  sspba  30656  shlej2i  31308  chpssati  32292  iunrnmptss  32494  mptssALT  32599  pmtrcnelor  33048  rspectopn  33857  zarmxt1  33870  bnj1408  35026  subfacp1lem6  35172  mthmpps  35569  bj-gabss  36923  qsss1  38277  cossss  38416  disjdmqscossss  38795  aomclem4  43046  cotrclrcl  43731  ovnsslelem  46558  isubgredgss  47865  fldcALTV  48320