Theorem 3sstr4g 3997

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3928

This theorem is referenced by:  rabss2  4037  unss2  4146  sslin  4202  intss  4929  ssopab2  5501  xpss12  5646  coss1  5809  coss2  5810  cnvss  5826  rnss  5892  ssres  5963  ssres2  5964  imass1  6061  imass2  6062  predpredss  6269  predrelss  6298  ssoprab2  7437  ressuppss  8139  tposss  8183  onovuni  8288  ss2ixp  8860  fodomfi  9237  fodomfiOLD  9257  coss12d  14914  isumsplit  15782  isumrpcl  15785  cvgrat  15825  gsumzf1o  19826  gsumzmhm  19851  gsumzinv  19859  fldc  20704  dsmmsubg  21685  qustgpopn  24040  metnrmlem2  24782  ovolsslem  25418  uniioombllem3  25519  ulmres  26330  xrlimcnp  26911  pntlemq  27545  cusgredg  29404  sspba  30706  shlej2i  31358  chpssati  32342  iunrnmptss  32544  mptssALT  32649  pmtrcnelor  33063  rspectopn  33850  zarmxt1  33863  bnj1408  35019  subfacp1lem6  35165  mthmpps  35562  bj-gabss  36916  qsss1  38270  cossss  38409  disjdmqscossss  38788  aomclem4  43039  cotrclrcl  43724  ovnsslelem  46551  isubgredgss  47858  fldcALTV  48313