Theorem 3sstr4g 3983

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3914

This theorem is referenced by:  ss2rabdv  4021  rabss2  4024  rabss2OLD  4025  unss2  4134  sslin  4190  intss  4917  ssopab2  5484  xpss12  5629  coss1  5794  coss2  5795  cnvss  5811  rnss  5878  ssres  5951  ssres2  5952  imass1  6049  imass2  6050  predpredss  6255  predrelss  6284  ssoprab2  7414  ressuppss  8113  tposss  8157  onovuni  8262  ss2ixp  8834  fodomfi  9196  fodomfiOLD  9214  coss12d  14879  isumsplit  15747  isumrpcl  15750  cvgrat  15790  gsumzf1o  19824  gsumzmhm  19849  gsumzinv  19857  fldc  20699  dsmmsubg  21680  qustgpopn  24035  metnrmlem2  24776  ovolsslem  25412  uniioombllem3  25513  ulmres  26324  xrlimcnp  26905  pntlemq  27539  cusgredg  29402  sspba  30707  shlej2i  31359  chpssati  32343  iunrnmptss  32545  mptssALT  32657  pmtrcnelor  33060  rspectopn  33880  zarmxt1  33893  bnj1408  35048  subfacp1lem6  35229  mthmpps  35626  bj-gabss  36979  qsss1  38326  cossss  38526  disjdmqscossss  38900  aomclem4  43149  cotrclrcl  43834  ovnsslelem  46657  isubgredgss  47964  fldcALTV  48431