Theorem 3sstr4g 3970

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

Syntax hints:   → wi 4   = wceq 1548   ⊆ wss 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-ss 3902

This theorem is referenced by:  ss2rabd  4006  rabss2  4011  rabss2OLD  4012  unss2  4119  sslin  4174  intss  4902  ssopab2  5491  xpss12  5636  coss1  5800  coss2  5801  cnvss  5817  rnss  5888  ssres  5962  ssres2  5963  imass1  6060  imass2  6061  predpredss  6263  predrelss  6292  ssoprab2  7428  ressuppss  8127  tposss  8171  onovuni  8276  ss2ixp  8852  fodomfi  9216  fodomfiOLD  9234  coss12d  14929  isumsplit  15800  isumrpcl  15803  cvgrat  15843  gsumzf1o  19882  gsumzmhm  19907  gsumzinv  19915  fldc  20760  dsmmsubg  21722  qustgpopn  24107  metnrmlem2  24848  ovolsslem  25473  uniioombllem3  25574  ulmres  26375  xrlimcnp  26954  pntlemq  27586  cusgredg  29515  sspba  30820  shlej2i  31472  chpssati  32456  iunrnmptss  32658  mptssALT  32770  pmtrcnelor  33176  rspectopn  34063  zarmxt1  34076  bnj1408  35233  subfacp1lem6  35428  mthmpps  35825  bj-gabss  37303  qsss1  38677  cossss  38897  disjdmqscossss  39288  aomclem4  43517  cotrclrcl  44201  ovnsslelem  47017  isubgredgss  48370  fldcALTV  48837