Theorem 3sstr4g 3987

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-ss 3919

This theorem is used by:  ss2rabd  4023  rabss2  4028  rabss2OLD  4029  unss2  4136  sslin  4191  intss  4932  ssopab2  5529  xpss12  5674  coss1  5839  coss2  5840  cnvss  5856  rnss  5927  ssres  6000  ssres2  6001  imass1  6101  imass2  6102  predpredss  6310  predrelss  6339  ssoprab2  7484  ressuppss  8184  tposss  8228  onovuni  8334  ss2ixp  8920  fodomfi  9285  coss12d  15045  isumsplit  15929  isumrpcl  15932  cvgrat  15972  gsumzf1o  20038  gsumzmhm  20063  gsumzinv  20071  fldc  20949  dsmmsubg  21955  qustgpopn  24345  metnrmlem2  25086  ovolsslem  25711  uniioombllem3  25812  ulmres  26619  xrlimcnp  27201  pntlemq  27833  cusgredg  29868  sspba  31192  shlej2i  31844  chpssati  32828  iunrnmptss  33023  mptssALT  33132  pmtrcnelor  33516  rspectopn  34362  zarmxt1  34375  bnj1408  35530  subfacp1lem6  35749  mthmpps  36146  bj-gabss  37664  qsss1  39028  cossss  39248  disjdmqscossss  39639  aomclem4  43883  cotrclrcl  44567  ovnsslelem  47373  isubgredgss  48766  fldcALTV  49232