Theorem 3sstr4g 3966

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  ss2rabd  4000  rabss2  4005  rabss2OLD  4006  sslin  4142  unss2  4188  intss  4932  ssopab2  5525  xpss12  5670  coss1  5838  coss2  5839  cnvss  5856  rnss  5927  ssres  6004  ssres2  6005  imass1  6065  imass2  6066  predpredss  6326  predrelss  6355  ssoprab2  7508  ressuppss  8225  tposss  8269  onovuni  8375  ss2ixp  8963  fodomfi  9329  coss12d  15151  isumsplit  16035  isumrpcl  16038  cvgrat  16078  gsumzf1o  20153  gsumzmhm  20178  gsumzinv  20186  fldc  21068  dsmmsubg  22076  qustgpopn  24466  metnrmlem2  25207  ovolsslem  25832  uniioombllem3  25933  ulmres  26742  xrlimcnp  27323  pntlemq  27955  cusgredg  30032  sspba  31356  shlej2i  32008  chpssati  32992  iunrnmptss  33228  mptssALT  33336  pmtrcnelor  33719  rspectopn  34566  zarmxt1  34579  bnj1408  35733  acwer1prc  35851  subfacp1lem6  36116  mthmpps  36513  bj-gabss  38025  qsss1  39418  cossss  39638  disjdmqscossss  40029  aomclem4  44250  cotrclrcl  44932  ovnsslelem  47773  isubgredgss  49166  fldcALTV  49632