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 ⊢ (𝜑 → 𝐶 ⊆ 𝐷)

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ss 3918

This theorem is referenced by:  ss2rabd  4024  rabss2  4029  rabss2OLD  4030  unss2  4139  sslin  4195  intss  4924  ssopab2  5494  xpss12  5639  coss1  5804  coss2  5805  cnvss  5821  rnss  5888  ssres  5962  ssres2  5963  imass1  6060  imass2  6061  predpredss  6266  predrelss  6295  ssoprab2  7426  ressuppss  8125  tposss  8169  onovuni  8274  ss2ixp  8848  fodomfi  9212  fodomfiOLD  9230  coss12d  14895  isumsplit  15763  isumrpcl  15766  cvgrat  15806  gsumzf1o  19841  gsumzmhm  19866  gsumzinv  19874  fldc  20717  dsmmsubg  21698  qustgpopn  24064  metnrmlem2  24805  ovolsslem  25441  uniioombllem3  25542  ulmres  26353  xrlimcnp  26934  pntlemq  27568  cusgredg  29497  sspba  30802  shlej2i  31454  chpssati  32438  iunrnmptss  32640  mptssALT  32753  pmtrcnelor  33173  rspectopn  34024  zarmxt1  34037  bnj1408  35192  subfacp1lem6  35379  mthmpps  35776  bj-gabss  37136  qsss1  38488  cossss  38688  disjdmqscossss  39062  aomclem4  43299  cotrclrcl  43983  ovnsslelem  46804  isubgredgss  48111  fldcALTV  48578