Theorem 3sstr4g 3961

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

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

This theorem is used by:  ss2rabd  3997  rabss2  4002  rabss2OLD  4003  sslin  4139  unss2  4185  intss  4928  ssopab2  5520  xpss12  5665  coss1  5832  coss2  5833  cnvss  5849  rnss  5920  ssres  5993  ssres2  5994  imass1  6053  imass2  6054  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  39228  cossss  39448  disjdmqscossss  39839  aomclem4  44059  cotrclrcl  44742  ovnsslelem  47570  isubgredgss  48963  fldcALTV  49429