Theorem 3sstr4g 3975

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906

This theorem is referenced by:  ss2rabd  4012  rabss2  4017  rabss2OLD  4018  unss2  4127  sslin  4183  intss  4911  ssopab2  5501  xpss12  5646  coss1  5810  coss2  5811  cnvss  5827  rnss  5894  ssres  5968  ssres2  5969  imass1  6066  imass2  6067  predpredss  6272  predrelss  6301  ssoprab2  7435  ressuppss  8133  tposss  8177  onovuni  8282  ss2ixp  8858  fodomfi  9222  fodomfiOLD  9240  coss12d  14934  isumsplit  15805  isumrpcl  15808  cvgrat  15848  gsumzf1o  19887  gsumzmhm  19912  gsumzinv  19920  fldc  20761  dsmmsubg  21723  qustgpopn  24085  metnrmlem2  24826  ovolsslem  25451  uniioombllem3  25552  ulmres  26353  xrlimcnp  26932  pntlemq  27564  cusgredg  29493  sspba  30798  shlej2i  31450  chpssati  32434  iunrnmptss  32635  mptssALT  32747  pmtrcnelor  33152  rspectopn  34011  zarmxt1  34024  bnj1408  35178  subfacp1lem6  35367  mthmpps  35764  bj-gabss  37242  qsss1  38616  cossss  38836  disjdmqscossss  39227  aomclem4  43485  cotrclrcl  44169  ovnsslelem  46988  isubgredgss  48341  fldcALTV  48808