Theorem 3sstr4g 3985

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

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

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 2123  ax-ext 2706

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

This theorem is referenced by:  ss2rabd  4022  rabss2  4027  rabss2OLD  4028  unss2  4137  sslin  4193  intss  4922  ssopab2  5492  xpss12  5637  coss1  5802  coss2  5803  cnvss  5819  rnss  5886  ssres  5960  ssres2  5961  imass1  6058  imass2  6059  predpredss  6264  predrelss  6293  ssoprab2  7424  ressuppss  8123  tposss  8167  onovuni  8272  ss2ixp  8846  fodomfi  9210  fodomfiOLD  9228  coss12d  14893  isumsplit  15761  isumrpcl  15764  cvgrat  15804  gsumzf1o  19839  gsumzmhm  19864  gsumzinv  19872  fldc  20715  dsmmsubg  21696  qustgpopn  24062  metnrmlem2  24803  ovolsslem  25439  uniioombllem3  25540  ulmres  26351  xrlimcnp  26932  pntlemq  27566  cusgredg  29446  sspba  30751  shlej2i  31403  chpssati  32387  iunrnmptss  32589  mptssALT  32702  pmtrcnelor  33122  rspectopn  33973  zarmxt1  33986  bnj1408  35141  subfacp1lem6  35328  mthmpps  35725  bj-gabss  37079  qsss1  38427  cossss  38627  disjdmqscossss  39001  aomclem4  43241  cotrclrcl  43925  ovnsslelem  46746  isubgredgss  48053  fldcALTV  48520