Theorem 3sstr4g 3988

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 3973	. 2 ⊢ (𝜑 → 𝐶 ⊆ 𝐵)
4		3sstr4g.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	sseqtrrdi 3976	1 ⊢ (𝜑 → 𝐶 ⊆ 𝐷)

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3919

This theorem is referenced by:  ss2rabd  4025  rabss2  4030  rabss2OLD  4031  unss2  4140  sslin  4196  intss  4925  ssopab2  5495  xpss12  5640  coss1  5805  coss2  5806  cnvss  5822  rnss  5889  ssres  5963  ssres2  5964  imass1  6061  imass2  6062  predpredss  6267  predrelss  6296  ssoprab2  7428  ressuppss  8127  tposss  8171  onovuni  8276  ss2ixp  8852  fodomfi  9216  fodomfiOLD  9234  coss12d  14899  isumsplit  15767  isumrpcl  15770  cvgrat  15810  gsumzf1o  19845  gsumzmhm  19870  gsumzinv  19878  fldc  20721  dsmmsubg  21702  qustgpopn  24068  metnrmlem2  24809  ovolsslem  25445  uniioombllem3  25546  ulmres  26357  xrlimcnp  26938  pntlemq  27572  cusgredg  29501  sspba  30806  shlej2i  31458  chpssati  32442  iunrnmptss  32643  mptssALT  32755  pmtrcnelor  33175  rspectopn  34026  zarmxt1  34039  bnj1408  35194  subfacp1lem6  35381  mthmpps  35778  bj-gabss  37138  qsss1  38498  cossss  38718  disjdmqscossss  39109  aomclem4  43366  cotrclrcl  44050  ovnsslelem  46871  isubgredgss  48178  fldcALTV  48645