Theorem 3sstr4g 3991

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

Syntax hints:   → wi 4   = wceq 1562   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-cleq 2756  df-ss 3923

This theorem is referenced by:  ss2rabd  4027  rabss2  4032  rabss2OLD  4033  unss2  4141  sslin  4196  intss  4929  ssopab2  5519  xpss12  5664  coss1  5829  coss2  5830  cnvss  5846  rnss  5917  ssres  5991  ssres2  5992  imass1  6092  imass2  6093  predpredss  6297  predrelss  6326  ssoprab2  7466  ressuppss  8165  tposss  8209  onovuni  8315  ss2ixp  8894  fodomfi  9258  coss12d  14987  isumsplit  15872  isumrpcl  15875  cvgrat  15915  gsumzf1o  19954  gsumzmhm  19979  gsumzinv  19987  fldc  20835  dsmmsubg  21797  qustgpopn  24182  metnrmlem2  24923  ovolsslem  25548  uniioombllem3  25649  ulmres  26453  xrlimcnp  27035  pntlemq  27667  cusgredg  29627  sspba  30932  shlej2i  31584  chpssati  32568  iunrnmptss  32767  mptssALT  32878  pmtrcnelor  33273  rspectopn  34166  zarmxt1  34179  bnj1408  35333  subfacp1lem6  35540  mthmpps  35937  bj-gabss  37425  qsss1  38799  cossss  39019  disjdmqscossss  39410  aomclem4  43639  cotrclrcl  44323  ovnsslelem  47139  isubgredgss  48492  fldcALTV  48959