Theorem 3sstr4g 3990

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3922

This theorem is used by:  ss2rabd  4026  rabss2  4031  rabss2OLD  4032  unss2  4140  sslin  4195  intss  4934  ssopab2  5531  xpss12  5676  coss1  5841  coss2  5842  cnvss  5858  rnss  5929  ssres  6002  ssres2  6003  imass1  6103  imass2  6104  predpredss  6309  predrelss  6338  ssoprab2  7478  ressuppss  8175  tposss  8219  onovuni  8325  ss2ixp  8904  fodomfi  9268  coss12d  15014  isumsplit  15899  isumrpcl  15902  cvgrat  15942  gsumzf1o  19986  gsumzmhm  20011  gsumzinv  20019  fldc  20896  dsmmsubg  21902  qustgpopn  24286  metnrmlem2  25027  ovolsslem  25652  uniioombllem3  25753  ulmres  26560  xrlimcnp  27142  pntlemq  27774  cusgredg  29783  sspba  31088  shlej2i  31740  chpssati  32724  iunrnmptss  32919  mptssALT  33028  pmtrcnelor  33420  rspectopn  34266  zarmxt1  34279  bnj1408  35433  subfacp1lem6  35685  mthmpps  36082  bj-gabss  37599  qsss1  38972  cossss  39192  disjdmqscossss  39583  aomclem4  43812  cotrclrcl  44496  ovnsslelem  47302  isubgredgss  48658  fldcALTV  49125