Theorem 3sstr4g 3989

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

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

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 2709

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

This theorem is referenced by:  ss2rabd  4026  rabss2  4031  rabss2OLD  4032  unss2  4141  sslin  4197  intss  4926  ssopab2  5504  xpss12  5649  coss1  5814  coss2  5815  cnvss  5831  rnss  5898  ssres  5972  ssres2  5973  imass1  6070  imass2  6071  predpredss  6276  predrelss  6305  ssoprab2  7438  ressuppss  8137  tposss  8181  onovuni  8286  ss2ixp  8862  fodomfi  9226  fodomfiOLD  9244  coss12d  14909  isumsplit  15777  isumrpcl  15780  cvgrat  15820  gsumzf1o  19858  gsumzmhm  19883  gsumzinv  19891  fldc  20734  dsmmsubg  21715  qustgpopn  24081  metnrmlem2  24822  ovolsslem  25458  uniioombllem3  25559  ulmres  26370  xrlimcnp  26951  pntlemq  27585  cusgredg  29515  sspba  30821  shlej2i  31473  chpssati  32457  iunrnmptss  32658  mptssALT  32770  pmtrcnelor  33191  rspectopn  34051  zarmxt1  34064  bnj1408  35218  subfacp1lem6  35407  mthmpps  35804  bj-gabss  37210  qsss1  38575  cossss  38795  disjdmqscossss  39186  aomclem4  43443  cotrclrcl  44127  ovnsslelem  46947  isubgredgss  48254  fldcALTV  48721