Theorem 3sstr4g 4037

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968

This theorem is referenced by:  rabss2  4078  unss2  4187  sslin  4243  intss  4969  ssopab2  5551  xpss12  5700  coss1  5866  coss2  5867  cnvss  5883  rnss  5950  ssres  6021  ssres2  6022  imass1  6119  imass2  6120  predpredss  6328  predrelss  6358  ssoprab2  7501  ressuppss  8208  tposss  8252  onovuni  8382  ss2ixp  8950  fodomfi  9350  fodomfiOLD  9370  coss12d  15011  isumsplit  15876  isumrpcl  15879  cvgrat  15919  gsumzf1o  19930  gsumzmhm  19955  gsumzinv  19963  fldc  20785  dsmmsubg  21763  qustgpopn  24128  metnrmlem2  24882  ovolsslem  25519  uniioombllem3  25620  ulmres  26431  xrlimcnp  27011  pntlemq  27645  cusgredg  29441  sspba  30746  shlej2i  31398  chpssati  32382  iunrnmptss  32578  mptssALT  32685  pmtrcnelor  33111  rspectopn  33866  zarmxt1  33879  bnj1408  35050  subfacp1lem6  35190  mthmpps  35587  bj-gabss  36936  qsss1  38290  cossss  38426  disjdmqscossss  38804  aomclem4  43069  cotrclrcl  43755  ovnsslelem  46575  isubgredgss  47851  uspgrimprop  47873  fldcALTV  48248