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 2733

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

This theorem is used by:  ss2rabd  4020  rabss2  4025  rabss2OLD  4026  unss2  4133  sslin  4188  intss  4929  ssopab2  5521  xpss12  5666  coss1  5833  coss2  5834  cnvss  5850  rnss  5921  ssres  5994  ssres2  5995  imass1  6054  imass2  6055  predpredss  6311  predrelss  6340  ssoprab2  7488  ressuppss  8200  tposss  8244  onovuni  8350  ss2ixp  8938  fodomfi  9304  coss12d  15125  isumsplit  16009  isumrpcl  16012  cvgrat  16052  gsumzf1o  20126  gsumzmhm  20151  gsumzinv  20159  fldc  21041  dsmmsubg  22049  qustgpopn  24439  metnrmlem2  25180  ovolsslem  25805  uniioombllem3  25906  ulmres  26715  xrlimcnp  27296  pntlemq  27928  cusgredg  30005  sspba  31329  shlej2i  31981  chpssati  32965  iunrnmptss  33159  mptssALT  33268  pmtrcnelor  33652  rspectopn  34499  zarmxt1  34512  bnj1408  35666  acwer1prc  35760  subfacp1lem6  35950  mthmpps  36347  bj-gabss  37848  qsss1  39227  cossss  39447  disjdmqscossss  39838  aomclem4  44058  cotrclrcl  44741  ovnsslelem  47569  isubgredgss  48962  fldcALTV  49428