Theorem 3sstr4g 3984

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ss 3916

This theorem is used by:  ss2rabd  4020  rabss2  4025  rabss2OLD  4026  unss2  4133  sslin  4188  intss  4929  ssopab2  5525  xpss12  5670  coss1  5837  coss2  5838  cnvss  5854  rnss  5925  ssres  5998  ssres2  5999  imass1  6099  imass2  6100  predpredss  6308  predrelss  6337  ssoprab2  7484  ressuppss  8186  tposss  8230  onovuni  8336  ss2ixp  8924  fodomfi  9289  coss12d  15070  isumsplit  15954  isumrpcl  15957  cvgrat  15997  gsumzf1o  20065  gsumzmhm  20090  gsumzinv  20098  fldc  20980  dsmmsubg  21988  qustgpopn  24378  metnrmlem2  25119  ovolsslem  25744  uniioombllem3  25845  ulmres  26656  xrlimcnp  27237  pntlemq  27869  cusgredg  29916  sspba  31240  shlej2i  31892  chpssati  32876  iunrnmptss  33070  mptssALT  33179  pmtrcnelor  33563  rspectopn  34410  zarmxt1  34423  bnj1408  35578  subfacp1lem6  35847  mthmpps  36244  bj-gabss  37746  qsss1  39108  cossss  39328  disjdmqscossss  39719  aomclem4  43963  cotrclrcl  44647  ovnsslelem  47453  isubgredgss  48846  fldcALTV  49312