Theorem 3sstr4i 3985

Description: Substitution of equality in both sides of a subclass relationship. (Contributed by NM, 13-Jan-1996.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)

Hypotheses

Ref	Expression
3sstr4.1	⊢ 𝐴 ⊆ 𝐵
3sstr4.2	⊢ 𝐶 = 𝐴
3sstr4.3	⊢ 𝐷 = 𝐵

Assertion

Ref	Expression
3sstr4i	⊢ 𝐶 ⊆ 𝐷

Proof of Theorem 3sstr4i

Step	Hyp	Ref	Expression
1		3sstr4.2	. . 3 ⊢ 𝐶 = 𝐴
2		3sstr4.1	. . 3 ⊢ 𝐴 ⊆ 𝐵
3	1, 2	eqsstri 3980	. 2 ⊢ 𝐶 ⊆ 𝐵
4		3sstr4.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	sseqtrri 3983	1 ⊢ 𝐶 ⊆ 𝐷

Syntax hints:   = 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:  relopabiv  5769  rncoss  5926  imassrn  6030  rnin  6104  inimass  6113  f1ossf1o  7073  ssoprab2i  7469  omopthlem2  8588  enssdom  8913  1sdom2dom  9154  rankval4  9779  cardf2  9855  r0weon  9922  dcomex  10357  axdc2lem  10358  fpwwe2lem1  10542  canthwe  10562  recmulnq  10875  npex  10897  axresscn  11059  mpoaddf  11120  mpomulf  11121  trclublem  14918  bpoly4  15982  2strop  17156  odlem1  19464  gexlem1  19508  pzriprnglem4  21439  psrbagsn  22018  bwth  23354  2ndcctbss  23399  uniioombllem4  25543  uniioombllem5  25544  eff1olem  26513  birthdaylem1  26917  zssno  28377  nvss  30668  lediri  31612  lejdiri  31614  sshhococi  31621  mayetes3i  31804  disjxpin  32663  imadifxp  32676  constrextdg2  33906  sxbrsigalem5  34445  eulerpartlemmf  34532  kur14lem6  35405  cvmlift2lem12  35508  bj-xpcossxp  37394  bj-rrhatsscchat  37441  mblfinlem4  37861  lclkrs2  41800  areaquad  43458  corclrcl  43948  corcltrcl  43980  relopabVD  45141  ovolval5lem3  46898  uspgrlimlem4  48237  setc1onsubc  49847